[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy
lp15 at cam.ac.uk
Fri Sep 14 16:17:16 CEST 2007
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.
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
> as soon as possible. Why not HOL.thy?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev