src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
Thu, 28 Aug 2014 16:58:27 +0200 blanchet merged minimize and auto_minimize
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT'
Mon, 04 Aug 2014 13:48:05 +0200 blanchet restored more sorting
Mon, 04 Aug 2014 12:28:42 +0200 blanchet rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
Fri, 01 Aug 2014 14:43:57 +0200 blanchet restored a bit of laziness
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tuning
Fri, 01 Aug 2014 14:43:57 +0200 blanchet eliminated needlessly complex message tail
Fri, 01 Aug 2014 14:43:57 +0200 blanchet eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
Fri, 01 Aug 2014 14:43:57 +0200 blanchet rationalized preplaying by eliminating (now superfluous) laziness
Fri, 01 Aug 2014 14:43:57 +0200 blanchet simplified minimization logic
Wed, 30 Jul 2014 23:52:56 +0200 blanchet use parallel preplay machinery also for one-line proofs
Wed, 30 Jul 2014 23:52:56 +0200 blanchet always minimize Sledgehammer results by default
Fri, 25 Jul 2014 11:26:23 +0200 blanchet don't lose 'minimize' flag before it reaches Isar proof text generation
Thu, 12 Jun 2014 17:10:12 +0200 blanchet renamed Sledgehammer options
Wed, 11 Jun 2014 11:28:46 +0200 blanchet removed old SMT module from Sledgehammer
Thu, 22 May 2014 03:29:36 +0200 blanchet tuning
Fri, 16 May 2014 19:14:00 +0200 blanchet correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
Thu, 13 Mar 2014 13:18:13 +0100 blanchet integrate SMT2 with Sledgehammer
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 19:32:02 +0100 blanchet renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
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'
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning
Fri, 31 Jan 2014 12:30:54 +0100 blanchet refactor large ML file
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure
less more (0) tip