src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
2014-05-21 blanchet 2014-05-21 avoid markup-generating @{make_string}
2014-05-16 blanchet 2014-05-16 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
2014-05-16 blanchet 2014-05-16 use 'simp add:' syntax in Sledgehammer rather than 'using'
2014-03-14 blanchet 2014-03-14 delayed construction of command (and of noncommercial check) + tuning
2014-03-13 blanchet 2014-03-13 simplified preplaying information
2014-03-13 blanchet 2014-03-13 honor the fact that the new Z3 can generate Isar proofs
2014-03-13 blanchet 2014-03-13 integrate SMT2 with Sledgehammer
2014-02-14 blanchet 2014-02-14 restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
2014-02-13 blanchet 2014-02-13 do the right thing with provers that exist only remotely (e.g. e_sine)
2014-02-13 blanchet 2014-02-13 repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial
2014-02-13 blanchet 2014-02-13 avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
2014-02-06 blanchet 2014-02-06 try right bunch of methods
2014-02-04 blanchet 2014-02-04 split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
2014-02-03 blanchet 2014-02-03 properly overwrite replay data from one compression iteration to another
2014-02-03 blanchet 2014-02-03 renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
2014-02-03 blanchet 2014-02-03 added 'smt' option to control generation of 'by smt' proofs
2014-02-03 blanchet 2014-02-03 renamed ML file
2014-02-03 blanchet 2014-02-03 tuning
2014-02-03 blanchet 2014-02-03 merged 'reconstructors' and 'proof methods'
2014-01-31 blanchet 2014-01-31 tuning
2014-01-31 blanchet 2014-01-31 moved ML code around
2014-01-31 blanchet 2014-01-31 compile
2014-01-31 blanchet 2014-01-31 guarded against exception
2014-01-31 blanchet 2014-01-31 refactor large ML file
2014-01-31 blanchet 2014-01-31 renamed many Sledgehammer ML files to clarify structure
2014-01-31 blanchet 2014-01-31 renamed ML file