[isabelle-dev] Old 'defs'

[Andreas Lochbihler]

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