src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
Thu, 22 May 2014 03:29:36 +0200 blanchet tuning
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Thu, 13 Feb 2014 13:16:17 +0100 blanchet avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
Mon, 03 Feb 2014 23:38:33 +0100 blanchet properly overwrite replay data from one compression iteration to another
Mon, 03 Feb 2014 23:20:12 +0100 blanchet tuning
Mon, 03 Feb 2014 19:32:02 +0100 blanchet renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
Mon, 03 Feb 2014 19:32:02 +0100 blanchet tuned behavior of 'smt' option
Mon, 03 Feb 2014 17:13:31 +0100 blanchet added 'smt' option to control generation of 'by smt' proofs
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods'
Mon, 03 Feb 2014 10:14:18 +0100 blanchet made SML/NJ happier
Mon, 03 Feb 2014 10:14:18 +0100 blanchet got rid of 'try0' step that is now redundant
Sun, 02 Feb 2014 20:53:51 +0100 blanchet rationalized threading of 'metis' arguments
Sun, 02 Feb 2014 20:53:51 +0100 blanchet tuning
Sun, 02 Feb 2014 20:53:51 +0100 blanchet made SML/NJ happier
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning
Fri, 31 Jan 2014 13:42:47 +0100 blanchet compile
Fri, 31 Jan 2014 12:30:54 +0100 blanchet refactor large ML file
less more (0) tip