On Sun, 24 Jul 2011, Alexander Krauss wrote:
Anyway, the standard procedure for removal of old stuff is to start
marking it as old or legacy in the NEWS, and emitting suitable
legacy_warnings.
I will follow that standard procedure, once all occurrences of the old
code generator invocations
On 07/25/2011 10:25 AM, Makarius wrote:
On Sun, 24 Jul 2011, Alexander Krauss wrote:
Anyway, the standard procedure for removal of old stuff is to start
marking it as old or legacy in the NEWS, and emitting suitable
legacy_warnings.
I will follow that standard procedure, once all
Anyway, the standard procedure for removal of old stuff is to start
marking it as old or legacy in the NEWS, and emitting suitable
legacy_warnings.
I will follow that standard procedure, once all occurrences of the old
code generator invocations are replaced.
Put in legacy warnings already
On 07/21/2011 04:25 PM, Steven Obua wrote:
Actually, there is a third code generator hidden somewhere in
Isabelle.
If you are talking about what I know under the name Compute Oracle,
then rest assured that it is hidden well enough that the chance of some
user accidentially confusing it with
Lukas already assured me of that. No worries here.
- Steven
On 22.07.2011, at 00:07, Alexander Krauss wrote:
On 07/21/2011 04:25 PM, Steven Obua wrote:
Actually, there is a third code generator hidden somewhere in
Isabelle.
If you are talking about what I know under the name Compute
