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
Wed, 18 Jul 2012 08:44:04 +0200 blanchet learn from minimized ATP proofs file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet use async manager to manage MaSh learners to make sure they get killed cleanly file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet added option to control which fact filter is used file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet make tracing an option file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet more implementation work on MaSh file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet started implementing MaSh client-side I/O file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet renamed Sledgehammer options file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet more code rationalization in relevance filter file | diff | annotate
Wed, 11 Jul 2012 21:43:19 +0200 blanchet further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer) file | diff | annotate
Wed, 23 May 2012 13:28:20 +0200 blanchet lower the monomorphization thresholds for less scalable provers file | diff | annotate
Sat, 21 Apr 2012 11:15:49 +0200 blanchet swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations file | diff | annotate
Wed, 21 Mar 2012 16:53:24 +0100 blanchet improve "remote_satallax" by exploiting unsat core file | diff | annotate
Tue, 20 Mar 2012 18:42:45 +0100 blanchet made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release file | diff | annotate
Tue, 20 Mar 2012 00:44:30 +0100 blanchet added "dont_preplay" alias file | diff | annotate
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations; file | diff | annotate
Thu, 15 Mar 2012 20:07:00 +0100 wenzelm prefer formally checked @{keyword} parser; file | diff | annotate
Mon, 06 Feb 2012 23:01:01 +0100 blanchet renamed type encoding file | diff | annotate
Sat, 04 Feb 2012 12:08:18 +0100 blanchet made option available to users (mostly for experiments) file | diff | annotate
Thu, 02 Feb 2012 12:42:05 +0100 blanchet include new SPASS by default if available file | diff | annotate
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file file | diff | annotate
Thu, 19 Jan 2012 21:37:12 +0100 blanchet renamed "sound" option to "strict" file | diff | annotate
Thu, 19 Jan 2012 21:37:12 +0100 blanchet lower timeout for preplay, now that we have more preplay methods file | diff | annotate
Thu, 01 Dec 2011 13:34:14 +0100 blanchet added "minimize" option for more control over automatic minimization file | diff | annotate
Thu, 01 Dec 2011 13:34:13 +0100 blanchet renamed "slicing" to "slice" file | diff | annotate
Wed, 16 Nov 2011 16:35:19 +0100 blanchet thread in additional options to minimizer file | diff | annotate
Wed, 16 Nov 2011 13:22:36 +0100 blanchet make metis reconstruction handling more flexible file | diff | annotate
Wed, 16 Nov 2011 09:42:27 +0100 blanchet parse lambda translation option in Metis file | diff | annotate
Fri, 23 Sep 2011 16:44:51 +0200 blanchet reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff) file | diff | annotate
Thu, 22 Sep 2011 19:42:06 +0200 blanchet take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime file | diff | annotate
Wed, 07 Sep 2011 13:50:17 +0200 blanchet parse new experimental '@' encodings file | diff | annotate
Wed, 07 Sep 2011 13:50:17 +0200 blanchet tuning file | diff | annotate
Wed, 07 Sep 2011 09:10:41 +0200 blanchet rationalize uniform encodings file | diff | annotate
Mon, 05 Sep 2011 14:42:31 +0200 blanchet fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]" file | diff | annotate
Fri, 02 Sep 2011 14:43:20 +0200 blanchet renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy) file | diff | annotate
Tue, 30 Aug 2011 16:07:45 +0200 blanchet extended simple types with polymorphism -- the implementation still needs some work though file | diff | annotate
Thu, 25 Aug 2011 14:25:07 +0200 blanchet rationalized option names -- mono becomes raw_mono and mangled becomes mono file | diff | annotate
Wed, 24 Aug 2011 11:17:33 +0200 blanchet more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac" file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet cleaner handling of polymorphic monotonicity inference file | diff | annotate
Tue, 09 Aug 2011 09:33:50 +0200 blanchet renamed E wrappers for consistency with CASC conventions file | diff | annotate
Tue, 26 Jul 2011 22:53:06 +0200 blanchet renamed "preds" encodings to "guards" file | diff | annotate
Fri, 01 Jul 2011 15:53:38 +0200 blanchet renamed "type_sys" to "type_enc", which is more accurate file | diff | annotate
Mon, 27 Jun 2011 14:56:28 +0200 blanchet added "sound" option to force Sledgehammer to be pedantically sound file | diff | annotate
Mon, 27 Jun 2011 13:52:47 +0200 blanchet removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway file | diff | annotate
Fri, 10 Jun 2011 12:01:15 +0200 blanchet removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them file | diff | annotate
Fri, 10 Jun 2011 12:01:15 +0200 blanchet fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day file | diff | annotate
Wed, 08 Jun 2011 08:47:43 +0200 blanchet killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true" file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet parse optional type system specification file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation file | diff | annotate
Mon, 30 May 2011 17:00:38 +0200 blanchet made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly file | diff | annotate
Mon, 30 May 2011 17:00:38 +0200 blanchet fixed syntax of min options file | diff | annotate
Mon, 30 May 2011 17:00:38 +0200 blanchet minimize with Metis if possible file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet try both "metis" and (on failure) "metisFT" in replay file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet handle non-auto try case of Sledgehammer better file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet renamed "Auto_Tools" "Try" file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet renamed "metis_timeout" to "preplay_timeout" and continued implementation file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet shorten minimizer command further, exploiting until-now-undocumented syntax file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet added syntax for specifying Metis timeout (currently used only by SMT solvers) file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet reintroduced Waldmeister but limit the number of remote threads created file | diff | annotate
less more (0) -100 -60 tip
isabelle