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
