src/HOL/ATP.thy
2017-08-07 blanchet 2017-08-07 tuning imports
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-20 steckerm 2014-09-20 Changed proof method to auto for custom Waldmeister lemma
2014-09-20 steckerm 2014-09-20 Minor fixes in ATP_Waldmeister
2014-09-02 steckerm 2014-09-02 Some work on the new waldmeister integration
2014-07-30 fleury 2014-07-30 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
2014-07-30 fleury 2014-07-30 imported patch hilbert_choice_support
2014-07-30 fleury 2014-07-30 imported patch satallax_proof_support_Sledgehammer
2014-06-16 blanchet 2014-06-16 simplified code
2014-06-16 blanchet 2014-06-16 moved code around
2014-06-16 fleury 2014-06-16 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
2014-05-13 blanchet 2014-05-13 hide more internal names
2013-10-18 blanchet 2013-10-18 killed more "no_atp"s
2013-09-09 blanchet 2013-09-09 move metis to new monomorphizer
2013-03-28 boehmes 2013-03-28 new, simpler implementation of monomorphization; old monomorphization code is still available as Legacy_Monomorphization; modified SMT integration to use the new monomorphization code
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-05-21 blanchet 2012-05-21 add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file
2011-12-14 blanchet 2011-12-14 added new proof redirection code
2011-11-16 blanchet 2011-11-16 compile
2011-08-09 blanchet 2011-08-09 load lambda-lifting structure earlier, so it can be used in Metis
2011-07-05 nik 2011-07-05 improved translation of lambdas in THF
2011-05-31 blanchet 2011-05-31 use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2010-10-26 blanchet 2010-10-26 reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
2010-10-25 haftmann 2010-10-25 moved sledgehammer to Plain; tuned dependencies
2010-10-05 blanchet 2010-10-05 tuned comments
2010-10-05 blanchet 2010-10-05 factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure