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

[Lawrence Paulson]

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.

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