[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.


More information about the isabelle-dev mailing list