src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
Thu, 13 Feb 2014 13:16:17 +0100 blanchet repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial
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
Thu, 06 Feb 2014 01:13:44 +0100 blanchet try right bunch of methods
Tue, 04 Feb 2014 23:11:18 +0100 blanchet split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
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:33:18 +0100 blanchet tuning
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 16:07:20 +0100 blanchet moved ML code around
Fri, 31 Jan 2014 13:42:47 +0100 blanchet compile
Fri, 31 Jan 2014 13:32:13 +0100 blanchet guarded against exception
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
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed ML file
less more (0) tip