src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
Sat, 14 Nov 2015 13:48:49 +0100 wenzelm more standard ML, to make SML/NJ more happy;
Tue, 10 Nov 2015 17:49:54 +0100 fleury generalized so that is also works for veriT proofs
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Wed, 08 Oct 2014 17:09:07 +0200 wenzelm added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
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 23:29:50 +0200 blanchet fine-tuned Isar reconstruction, esp. boolean simplifications
Fri, 01 Aug 2014 20:44:51 +0200 blanchet careful when compressing 'obtains'
Fri, 01 Aug 2014 20:15:41 +0200 blanchet try to get rid of skolems first
Fri, 01 Aug 2014 19:32:46 +0200 blanchet no need to 'obtain' variables not in formula
Thu, 31 Jul 2014 00:45:55 +0200 blanchet cascading timeout in parallel evaluation, to rapidly find optimum
Wed, 30 Jul 2014 00:50:41 +0200 blanchet also try 'metis' with 'full_types'
Tue, 24 Jun 2014 08:19:22 +0200 blanchet don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)
Thu, 12 Jun 2014 17:10:12 +0200 blanchet renamed Sledgehammer options
Mon, 02 Jun 2014 22:38:46 +0200 blanchet avoid division by 0
Thu, 22 May 2014 03:29:36 +0200 blanchet tuning
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
Wed, 05 Feb 2014 11:37:32 +0100 blanchet more exception cleanup + more liberal compressions of steps that timed out
Wed, 05 Feb 2014 11:22:36 +0100 blanchet tuned code to avoid noncanonical (and risky) exception handling
Wed, 05 Feb 2014 09:25:48 +0100 blanchet got rid of indices
Wed, 05 Feb 2014 09:07:08 +0100 blanchet corrected wrong 'meth :: _' pattern maching + tuned code
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 tweaked handling of 'hopeless' methods
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)
Tue, 04 Feb 2014 00:04:55 +0100 blanchet tuning
Tue, 04 Feb 2014 00:01:54 +0100 blanchet more liberal step merging
Mon, 03 Feb 2014 23:44:39 +0100 blanchet don't lose additional outcomes
Mon, 03 Feb 2014 23:20:12 +0100 blanchet tuning
Mon, 03 Feb 2014 19:32:02 +0100 blanchet generate comments in Isar proofs
Mon, 03 Feb 2014 19:32:02 +0100 blanchet allow merging of steps with subproofs
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file
Mon, 03 Feb 2014 14:30:16 +0100 blanchet when merging, don't try methods that failed or timed out for either of the steps for the combined step
Mon, 03 Feb 2014 11:58:38 +0100 blanchet tuned data structure
Mon, 03 Feb 2014 11:30:53 +0100 blanchet more flexible compression, choosing whichever proof method works
Mon, 03 Feb 2014 10:14:18 +0100 blanchet tuning
Mon, 03 Feb 2014 10:14:18 +0100 blanchet better time slack, to account for ultra-quick proof methods
Mon, 03 Feb 2014 10:14:18 +0100 blanchet crucial fix: use right version of the step
Mon, 03 Feb 2014 10:14:18 +0100 blanchet more thorough, hybrid compression
Mon, 03 Feb 2014 10:14:18 +0100 blanchet tuning
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 refactoring of data structure (step 2)
Sun, 02 Feb 2014 20:53:51 +0100 blanchet refactor data structure (step 1)
Sun, 02 Feb 2014 20:53:51 +0100 blanchet tuned factor
Sun, 02 Feb 2014 20:53:51 +0100 blanchet take intersection rather than union of methods when merging steps -- more efficient and natural
Sun, 02 Feb 2014 20:53:51 +0100 blanchet merge proof methods
Sun, 02 Feb 2014 20:53:51 +0100 blanchet simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
Sun, 02 Feb 2014 20:53:51 +0100 blanchet reset timing information after changes
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 tuning
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 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure
less more (0) tip