[isabelle-dev] Old 'defs'
andreas.lochbihler at inf.ethz.ch
Mon Jul 7 08:36:30 CEST 2014
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
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev