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

[Lawrence Paulson]

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