[isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

[Lawrence Paulson]

> 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. 

Larry
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170826/c26ae160/attachment-0002.html>