src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
2016-04-02 ago prefer infix operations;
2016-03-28 ago early warning when Sledgehammer finds a proof
2016-03-28 ago refined experimental option of Sledgehammer
2016-03-07 ago File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
2016-03-05 ago tuned signature -- clarified modules;
2016-02-23 ago more canonical names
2015-12-19 ago cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
2015-10-05 ago added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
2015-08-19 ago proper check for Windows executables;
2015-08-13 ago tuned signature, in accordance to sortBy in Scala;
2015-03-04 ago tuned signature -- prefer qualified names;
2015-03-03 ago SPASS-Pirate is now called Pirate
2014-12-22 ago separate module Random;
2014-10-31 ago discontinued obsolete Output.urgent_message;
2014-09-09 ago Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new
2014-09-02 ago Some work on the new waldmeister integration
2014-08-28 ago merged minimize and auto_minimize
2014-08-05 ago tuning
2014-08-04 ago default on 'metis' for ATPs if preplaying is disabled
2014-08-04 ago rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
2014-08-01 ago restored a bit of laziness
2014-08-01 ago honor 'try0' also for one-liners
2014-08-01 ago tuning
2014-08-01 ago eliminated needlessly complex message tail
2014-08-01 ago eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
2014-08-01 ago rationalized preplaying by eliminating (now superfluous) laziness
2014-08-01 ago simplified minimization logic
2014-07-30 ago use parallel preplay machinery also for one-line proofs
2014-07-30 ago always minimize Sledgehammer results by default
2014-07-30 ago imported patch satallax_proof_support_Sledgehammer
2014-07-25 ago avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
2014-07-01 ago speed up MaSh a bit
2014-06-16 ago integrated new Waldmeister code with 'sledgehammer' command
2014-06-16 ago fixed parsing of one-argument 'file()' in TSTP files
2014-06-16 ago simplified code
2014-06-16 ago Moving the remote prefix deleting on Sledgehammer's side
2014-06-16 ago add support for Isar reconstruction for thf1 ATP provers like Leo-II.
2014-06-12 ago renamed Sledgehammer options
2014-06-02 ago basic setup for zipperposition prover
2014-05-22 ago tuning
2014-03-21 ago more qualified names;
2014-02-13 ago avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
2014-02-03 ago properly overwrite replay data from one compression iteration to another
2014-02-03 ago tuning
2014-02-03 ago renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
2014-02-03 ago tuned behavior of 'smt' option
2014-02-03 ago added 'smt' option to control generation of 'by smt' proofs
2014-02-03 ago renamed ML file
2014-02-03 ago merged 'reconstructors' and 'proof methods'
2014-02-03 ago made SML/NJ happier
2014-02-03 ago got rid of 'try0' step that is now redundant
2014-02-02 ago rationalized threading of 'metis' arguments
2014-02-02 ago tuning
2014-02-02 ago made SML/NJ happier
2014-01-31 ago tuning
2014-01-31 ago compile
2014-01-31 ago refactor large ML file