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

[Christian Urban]

Lawrence Paulson writes:
 > 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?

The nominal methods happily coexists with the axiom-of-choice. 
The earlier attempt to implement them on an axiom-of-choice-free
basis was a deadend...this can happen in science ;o)

  -- Christian