[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy

Tobias Nipkow nipkow at in.tum.de
Sun Sep 16 18:53:20 CEST 2007

That's fine with me. I would not insist on breaking the current careful 
separation of the constructive part of HOL.


Lawrence Paulson schrieb:
>   So, metis becomes available just before List.thy? This might be a good 
> compromise.
> Larry
> On 14 Sep 2007, at 15:26, Florian Haftmann wrote:
>> I would still argue that it is a good idea to have a non-Hilbertian
>> entrance point to HOL (PreList);  anyway there should be no problem to
>> import Hilbert_Choice before List and then setup Metis and Sledgehammer.
> ------------------------------------------------------------------------
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list