src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
Fri, 14 Mar 2014 11:05:45 +0100 blanchet debugging stuff
Fri, 14 Mar 2014 11:05:44 +0100 blanchet more simplification of trivial steps
Fri, 14 Mar 2014 11:05:37 +0100 blanchet tuning
Thu, 13 Mar 2014 13:18:14 +0100 blanchet tuning
Thu, 13 Mar 2014 13:18:14 +0100 blanchet simplified preplaying information
Thu, 13 Mar 2014 13:18:13 +0100 blanchet integrate SMT2 with Sledgehammer
Thu, 06 Mar 2014 10:12:47 +0100 wenzelm tuned signature;
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
Tue, 04 Feb 2014 23:11:18 +0100 blanchet more generous Isar proof compression -- try to remove failing steps
Tue, 04 Feb 2014 23:11:18 +0100 blanchet do a second phase of proof compression after minimization
Tue, 04 Feb 2014 23:11:18 +0100 blanchet tuned code
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:59:36 +0100 blanchet rationalized lists of methods
Mon, 03 Feb 2014 23:49:01 +0100 blanchet extended method list
Mon, 03 Feb 2014 19:32:02 +0100 blanchet generate comments in Isar proofs
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 19:32:02 +0100 blanchet proper fresh name generation
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'
Mon, 03 Feb 2014 13:37:23 +0100 blanchet tuning
Mon, 03 Feb 2014 11:58:38 +0100 blanchet tuned data structure
Mon, 03 Feb 2014 11:37:48 +0100 blanchet tuned data structure
Mon, 03 Feb 2014 10:14:18 +0100 blanchet less aggressive evaluation
Mon, 03 Feb 2014 10:14:18 +0100 blanchet added a new version of 'metis' to the mix
Mon, 03 Feb 2014 10:14:18 +0100 blanchet implemented new 'try0_isar' semantics
Mon, 03 Feb 2014 10:14:18 +0100 blanchet got rid of 'try0' step that is now redundant
Mon, 03 Feb 2014 10:14:18 +0100 blanchet centralize more preplaying
Mon, 03 Feb 2014 10:14:18 +0100 blanchet centralize preplaying
Mon, 03 Feb 2014 10:14:18 +0100 blanchet tuned
Sun, 02 Feb 2014 20:53:51 +0100 blanchet more data structure rationalization
Sun, 02 Feb 2014 20:53:51 +0100 blanchet more data structure rationalization
Sun, 02 Feb 2014 20:53:51 +0100 blanchet rationalized threading of 'metis' arguments
Sun, 02 Feb 2014 20:53:51 +0100 blanchet refactored data structure (step 3)
Sun, 02 Feb 2014 20:53:51 +0100 blanchet unform treatment of preplay_timeout = 0 and > 0
Sun, 02 Feb 2014 20:53:51 +0100 blanchet use Skolem proof methods appropriately
Sun, 02 Feb 2014 20:53:51 +0100 blanchet simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
Fri, 31 Jan 2014 19:16:41 +0100 blanchet generalized preplaying infrastructure to store various results for various methods
Fri, 31 Jan 2014 18:43:16 +0100 blanchet added a 'trace' option
Fri, 31 Jan 2014 18:43:16 +0100 blanchet moved code around
Fri, 31 Jan 2014 18:43:16 +0100 blanchet added 'algebra' to the mix
Fri, 31 Jan 2014 18:43:16 +0100 blanchet more informative trace
Fri, 31 Jan 2014 16:41:54 +0100 blanchet better tracing + syntactically correct 'metis' calls
Fri, 31 Jan 2014 16:26:43 +0100 blanchet tuned ML function names
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 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure
Thu, 30 Jan 2014 14:37:53 +0100 blanchet renamed Sledgehammer options for symmetry between positive and negative versions
Thu, 19 Dec 2013 13:43:21 +0100 blanchet made timeouts in Sledgehammer not be 'option's -- simplified lots of code
Thu, 21 Nov 2013 12:29:29 +0100 blanchet fixed spying so that the envirnoment variables are queried at run-time not at build-time
Tue, 19 Nov 2013 18:34:04 +0100 blanchet tuning
Thu, 17 Oct 2013 01:34:34 +0200 blanchet added comment
Tue, 15 Oct 2013 15:31:18 +0200 blanchet use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
Fri, 04 Oct 2013 11:52:10 +0200 blanchet run fewer provers in "try" mode
Fri, 04 Oct 2013 11:28:28 +0200 blanchet count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)
Mon, 23 Sep 2013 14:53:43 +0200 blanchet added "spy" option to Sledgehammer
Fri, 20 Sep 2013 22:39:30 +0200 blanchet merged "isar_try0" and "isar_minimize" options
Fri, 20 Sep 2013 22:39:30 +0200 blanchet hardcoded obscure option
less more (0) -300 -100 -60 tip