Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
Mon, 03 Feb 2014 11:37:48 +0100 blanchet tuned data structure 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 added a new version of 'metis' to the mix file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet implemented new 'try0_isar' semantics file | diff | annotate
Mon, 03 Feb 2014 10:14:18 +0100 blanchet got rid of 'try0' step that is now redundant 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 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 unform treatment of preplay_timeout = 0 and > 0 file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet use Skolem proof methods appropriately 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
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 added a 'trace' option file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet moved code around file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet added 'algebra' to the mix file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet more informative trace file | diff | annotate
Fri, 31 Jan 2014 16:41:54 +0100 blanchet better tracing + syntactically correct 'metis' calls 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 16:07:20 +0100 blanchet moved ML code around file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure file | diff | annotate | base
Thu, 30 Jan 2014 14:37:53 +0100 blanchet renamed Sledgehammer options for symmetry between positive and negative versions file | diff | annotate
Thu, 19 Dec 2013 13:43:21 +0100 blanchet made timeouts in Sledgehammer not be 'option's -- simplified lots of code file | diff | annotate
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 file | diff | annotate
Tue, 19 Nov 2013 18:34:04 +0100 blanchet tuning file | diff | annotate
Thu, 17 Oct 2013 01:34:34 +0200 blanchet added comment file | diff | annotate
Tue, 15 Oct 2013 15:31:18 +0200 blanchet use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available file | diff | annotate
Fri, 04 Oct 2013 11:52:10 +0200 blanchet run fewer provers in "try" mode file | diff | annotate
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) file | diff | annotate
Mon, 23 Sep 2013 14:53:43 +0200 blanchet added "spy" option to Sledgehammer file | diff | annotate
Fri, 20 Sep 2013 22:39:30 +0200 blanchet merged "isar_try0" and "isar_minimize" options file | diff | annotate
Fri, 20 Sep 2013 22:39:30 +0200 blanchet hardcoded obscure option file | diff | annotate
Fri, 20 Sep 2013 22:39:30 +0200 blanchet hard-coded an obscure option file | diff | annotate
Fri, 20 Sep 2013 22:39:30 +0200 blanchet use configuration mechanism for low-level tracing file | diff | annotate
Fri, 20 Sep 2013 22:39:30 +0200 blanchet took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired file | diff | annotate
Fri, 20 Sep 2013 22:39:30 +0200 blanchet tuning (use a blacklist instead of a whitelist) file | diff | annotate
Thu, 22 Aug 2013 23:03:21 +0200 blanchet fixed subtle bug with "take" + thread overlord through file | diff | annotate
Thu, 22 Aug 2013 16:03:13 +0200 blanchet have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation file | diff | annotate
Sat, 17 Aug 2013 22:45:48 +0200 wenzelm prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options; file | diff | annotate
Sat, 17 Aug 2013 22:15:45 +0200 wenzelm some protocol to determine provers according to ML; file | diff | annotate
Sat, 17 Aug 2013 19:54:16 +0200 wenzelm always enable "minimize" to simplify interaction model; file | diff | annotate
Sat, 17 Aug 2013 19:13:28 +0200 wenzelm sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel; file | diff | annotate
Sat, 17 Aug 2013 12:21:25 +0200 wenzelm eliminated pointless subgoal argument; file | diff | annotate
Sat, 17 Aug 2013 12:13:53 +0200 wenzelm more direct sledgehammer configuration via mode = Normal_Result and output_result; file | diff | annotate
Mon, 12 Aug 2013 17:57:51 +0200 wenzelm clarified Query_Operation.register: avoid hard-wired parallel policy; file | diff | annotate
Thu, 08 Aug 2013 14:24:21 +0200 wenzelm dockable window for Sledgehammer, based on asynchronous/parallel query operation; file | diff | annotate
Sat, 13 Jul 2013 21:02:41 +0200 wenzelm merged file | diff | annotate
Sat, 13 Jul 2013 00:50:49 +0200 wenzelm hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function); file | diff | annotate
Fri, 12 Jul 2013 23:45:05 +0200 wenzelm system options for Isabelle/HOL proof tools; file | diff | annotate
Fri, 12 Jul 2013 22:41:25 +0200 smolkas added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases file | diff | annotate
Tue, 09 Jul 2013 18:45:06 +0200 smolkas completely rewrote SH compress; added two parameters for experimentation/fine grained control file | diff | annotate
Tue, 11 Jun 2013 16:13:19 -0400 smolkas make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation file | diff | annotate
Tue, 21 May 2013 09:02:58 +0200 blanchet added compatibility alias file | diff | annotate
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer file | diff | annotate
Wed, 15 May 2013 23:00:17 +0200 wenzelm merged; file | diff | annotate
Wed, 15 May 2013 22:30:24 +0200 wenzelm clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x; file | diff | annotate
less more (0) -100 -60 tip
isabelle