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

[Tobias Nipkow]

I would appreciate having at least metis early on. I have recently 
wasted some time trying to figure out the details of a 
sledgehammer/metis proof in order to add it to List.

Tobias

Lawrence Paulson schrieb:
> 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. We previously put some effort into making  
> virtually all of HOL independent of the axiom of choice, so this  
> would be a reversal. However, I don't know of anybody who has  
> actually taken advantage of the AC-free part; in particular, I don't  
> think that the use of nominal methods requires this any more. Can  
> anybody comment?
> 
> Larry
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev