On Mon, 7 Jul 2014, Andreas Lochbihler wrote:
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.
This use is no counter example yet, and very rare in practice.
IIRC, Florian Haftmann made the overloading target to include such
boundary cases, or rather he did not do anything specific to exclude them.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
