[isabelle-dev] Code generation in Isabelle
Alexander Krauss
krauss at in.tum.de
Sun Jul 24 21:57:01 CEST 2011
>> 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 now, as they will alert users who
accidentially type the wrong commands (remember our experience with the
methods "evaluation" vs. "eval" last week). You don't have to wait with
this until all else is resolved.
Alex
More information about the isabelle-dev
mailing list