> On 25 Aug 2017, at 20:14, Viorel Preoteasa <viorel.preote...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
