Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
Mon, 01 Feb 2016 19:57:58 +0100 blanchet preplaying of 'smt' and 'metis' more in sync with actual method file | diff | annotate
Sat, 14 Nov 2015 13:48:49 +0100 wenzelm more standard ML, to make SML/NJ more happy; file | diff | annotate
Tue, 10 Nov 2015 17:49:54 +0100 fleury generalized so that is also works for veriT proofs file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Wed, 08 Oct 2014 17:09:07 +0200 wenzelm added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N}; file | diff | annotate
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 file | diff | annotate
Fri, 01 Aug 2014 23:29:50 +0200 blanchet fine-tuned Isar reconstruction, esp. boolean simplifications file | diff | annotate
Fri, 01 Aug 2014 20:44:51 +0200 blanchet careful when compressing 'obtains' file | diff | annotate
Fri, 01 Aug 2014 20:15:41 +0200 blanchet try to get rid of skolems first file | diff | annotate
Fri, 01 Aug 2014 19:32:46 +0200 blanchet no need to 'obtain' variables not in formula file | diff | annotate
Thu, 31 Jul 2014 00:45:55 +0200 blanchet cascading timeout in parallel evaluation, to rapidly find optimum file | diff | annotate
Wed, 30 Jul 2014 00:50:41 +0200 blanchet also try 'metis' with 'full_types' file | diff | annotate
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) file | diff | annotate
Thu, 12 Jun 2014 17:10:12 +0200 blanchet renamed Sledgehammer options file | diff | annotate
Mon, 02 Jun 2014 22:38:46 +0200 blanchet avoid division by 0 file | diff | annotate
Thu, 22 May 2014 03:29:36 +0200 blanchet tuning file | diff | annotate
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 file | diff | annotate
Wed, 05 Feb 2014 11:37:32 +0100 blanchet more exception cleanup + more liberal compressions of steps that timed out file | diff | annotate
Wed, 05 Feb 2014 11:22:36 +0100 blanchet tuned code to avoid noncanonical (and risky) exception handling file | diff | annotate
Wed, 05 Feb 2014 09:25:48 +0100 blanchet got rid of indices file | diff | annotate
Wed, 05 Feb 2014 09:07:08 +0100 blanchet corrected wrong 'meth :: _' pattern maching + tuned code file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet more generous Isar proof compression -- try to remove failing steps file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet tweaked handling of 'hopeless' methods file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet tuned code file | diff | annotate
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) file | diff | annotate
Tue, 04 Feb 2014 00:04:55 +0100 blanchet tuning file | diff | annotate
Tue, 04 Feb 2014 00:01:54 +0100 blanchet more liberal step merging file | diff | annotate
Mon, 03 Feb 2014 23:44:39 +0100 blanchet don't lose additional outcomes file | diff | annotate
Mon, 03 Feb 2014 23:20:12 +0100 blanchet tuning file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet generate comments in Isar proofs file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet allow merging of steps with subproofs file | diff | annotate
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file file | diff | annotate
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 file | diff | annotate
Mon, 03 Feb 2014 11:58:38 +0100 blanchet tuned data structure file | diff | annotate
Mon, 03 Feb 2014 11:30:53 +0100 blanchet more flexible compression, choosing whichever proof method works file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet tuning file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet better time slack, to account for ultra-quick proof methods file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet crucial fix: use right version of the step file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet more thorough, hybrid compression file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet tuning file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet centralize more preplaying file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet centralize preplaying file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet tuned file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet more data structure rationalization file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet more data structure rationalization file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet refactoring of data structure (step 2) file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet refactor data structure (step 1) file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet tuned factor file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet take intersection rather than union of methods when merging steps -- more efficient and natural file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet merge proof methods file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet reset timing information after changes file | diff | annotate
Fri, 31 Jan 2014 19:16:41 +0100 blanchet generalized preplaying infrastructure to store various results for various methods file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 16:26:43 +0100 blanchet tuned ML function names file | diff | annotate
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure file | diff | annotate | base
less more (0) tip
isabelle