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

[Lawrence Paulson]

It needs at least Hilbert_Choice. It could go before Datatype. Some  
details need to be worked out to ensure that all theorems in Main.thy  
get converted to clause form.
Larry

On 14 Sep 2007, at 14:46, Florian Haftmann wrote:

> A PreList-Sledgehammer would be a nice thing to have, but it is not
> crucial.  Anyway I agree with Tobias that Metis itself should be  
> offered
> as soon as possible.  Why not HOL.thy?

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