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

[Tobias Nipkow]

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

Tobias

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