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

[Florian Haftmann]

> Florian has suggested making sledgehammer available earlier in the  
> construction of Main, before PreList at least. This could be useful  
> to developers. However, it requires Hilbert_Choice, which must also  
> be introduced earlier.

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?

Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20070914/fa2278cb/attachment-0002.vcf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20070914/fa2278cb/attachment.sig>