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_preplay.ML
Fri, 05 Mar 2021 16:09:42 +0100 wenzelm clarified signature --- augment existing structure Time; file | diff | annotate
Thu, 22 Oct 2020 15:18:08 +0200 desharna Tuned isar_step datatype file | diff | annotate
Wed, 21 Oct 2020 17:31:15 +0200 desharna Tuned isar_proof datatype file | diff | annotate
Thu, 29 Oct 2020 16:07:41 +0100 desharna Added smt (verit) to Sledgehammer's proof preplay. file | diff | annotate
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches; file | diff | annotate
Sat, 02 Apr 2016 23:29:05 +0200 wenzelm prefer infix operations; file | diff | annotate
Sat, 05 Mar 2016 17:01:45 +0100 wenzelm tuned signature -- clarified modules; file | diff | annotate
Mon, 01 Feb 2016 19:57:58 +0100 blanchet preplaying of 'smt' and 'metis' more in sync with actual method file | diff | annotate
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML; file | diff | annotate
Mon, 22 Jun 2015 16:56:03 +0200 blanchet keep 'Pure.all' in goals when preplaying 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, 24 Sep 2014 15:46:11 +0200 blanchet tuning file | diff | annotate
Thu, 28 Aug 2014 16:58:27 +0200 blanchet made trace more informative when minimization is enabled file | diff | annotate
Mon, 04 Aug 2014 11:54:23 +0200 blanchet slightly earlier exit from preplaying file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet rationalized preplaying by eliminating (now superfluous) laziness file | diff | annotate
Thu, 31 Jul 2014 00:45:55 +0200 blanchet cascading timeout in parallel evaluation, to rapidly find optimum file | diff | annotate
Thu, 22 May 2014 03:29:36 +0200 blanchet tuning file | diff | annotate
Thu, 13 Mar 2014 13:18:14 +0100 blanchet simplified preplaying information 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
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 01:03:28 +0100 blanchet tuning 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:38:33 +0100 blanchet properly overwrite replay data from one compression iteration to another 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 keep all proof methods in data structure until the end, to enhance debugging output file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet proper fresh name generation file | diff | annotate
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file file | diff | annotate
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods' file | diff | annotate
Mon, 03 Feb 2014 14:35:19 +0100 blanchet added 'smt' as a proof method file | diff | annotate
Mon, 03 Feb 2014 11:58:38 +0100 blanchet tuned data structure file | diff | annotate
Mon, 03 Feb 2014 11:37:48 +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 less aggressive evaluation 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 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
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 rationalized threading of 'metis' arguments file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet refactored data structure (step 3) 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 unform treatment of preplay_timeout = 0 and > 0 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 code 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 18:43:16 +0100 blanchet added 'algebra' to the mix 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