[isabelle-dev] Old 'defs'

[Makarius]

Are there remaining uses of the old 'defs' command?  It is not localized, 
and somehow an odd side-entry to the normal concept of definitional 
specifications in contempory Isabelle (which goes through 
Local_Theory.define instead of bare-bones foundations).

A hypersearch over Isabelle/251ef0202e71 and AFP/0576573b7840 shows very 
few occurrences of old 'defs', mainly in the form "defs (overloaded)". 
Isn't 'overloading' + 'definition' the canonical way to to that today? 
Or are fine points that do require the old form?

We've already managed to eliminate old 'axioms' some time ago.  So we 
could mark 'defs' as legacy now, and remove it eventually.


 	Makarius