[isabelle-dev] Old 'defs'

[Makarius]

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