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
