[isabelle-dev] Code generation in Isabelle

[Alexander Krauss]

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