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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
