There's one use in JinjaThreads which does not fit into the overloading scope: The
constants sc_spurious_wakeups are declared in MM/SC_Collections.thy and MM/SC.thy, but
intentionally not defined. This expresses that the remaining proofs are independent of the
value of the constant, which is in fact just a configuration option. Only later, in
Execute/SC_Schedulers, there is the definition that sets this configuration option.
One could convert this into overloading+definition, but it would be a very degenerate form
of overloading, as the configuration option is a plain boolean, there are no type
variables involved.
Andreas
On 05/07/14 17:15, Makarius wrote:
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
