[isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice
lp15 at cam.ac.uk
Sat Aug 26 14:06:20 CEST 2017
> On 25 Aug 2017, at 20:14, Viorel Preoteasa <viorel.preoteasa at aalto.fi> wrote:
> One possible solution:
> Add the new class in Complete_Lattice.thy, replacing the existing class
> Prove the instantiations and the complete_linearord subclass later
> in Hilbert_Choice.
> On the other hand, it seems inconvenient to have the Hilbert Choice
> to depend on so many other theories.
I’d prefer this provided the instantiations aren’t needed earlier.
The delay in the introduction of the Axiom of Choice is partly historical, but it’s worth noting how much of HOL can be developed without it.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev