Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -300 -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
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, 19 Dec 2013 10:15:12 +0100 blanchet simplified data structure file | diff | annotate
Thu, 19 Dec 2013 09:28:20 +0100 blanchet tuning file | diff | annotate
Wed, 18 Dec 2013 22:55:20 +0100 blanchet parse SPASS-Pirate types file | diff | annotate
Mon, 16 Dec 2013 23:36:54 +0100 blanchet fixed source of 'Subscript' exception file | diff | annotate
Mon, 16 Dec 2013 23:05:16 +0100 blanchet handle Skolems gracefully for SPASS as well file | diff | annotate
Tue, 19 Nov 2013 19:36:24 +0100 blanchet more refactoring to accommodate SMT proofs file | diff | annotate
Tue, 19 Nov 2013 17:37:35 +0100 blanchet refactoring file | diff | annotate
Tue, 19 Nov 2013 16:48:50 +0100 blanchet refactored file | diff | annotate
Thu, 14 Nov 2013 19:54:10 +0100 blanchet implemented 'tptp_translate' file | diff | annotate
Thu, 17 Oct 2013 20:49:19 +0200 blanchet generate a comment storing the goal nickname in "learn_prover" file | diff | annotate
Thu, 17 Oct 2013 01:10:08 +0200 blanchet if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice file | diff | annotate
Thu, 17 Oct 2013 01:04:00 +0200 blanchet if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts" file | diff | annotate
Thu, 10 Oct 2013 01:17:37 +0200 blanchet simplify fudge factor code file | diff | annotate
Wed, 09 Oct 2013 17:21:28 +0200 blanchet cleanup SMT-related config options file | diff | annotate
Wed, 09 Oct 2013 15:39:34 +0200 blanchet use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected) file | diff | annotate
Tue, 08 Oct 2013 22:33:05 +0200 blanchet higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False" file | diff | annotate
Mon, 30 Sep 2013 17:47:50 +0200 blanchet added experimental configuration options to tune use of builtin symbols in SMT file | diff | annotate
Mon, 30 Sep 2013 13:59:07 +0200 blanchet minor tweak to error message 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
Thu, 12 Sep 2013 22:10:57 +0200 blanchet prefixed types and some functions with "atp_" for disambiguation file | diff | annotate
Wed, 11 Sep 2013 22:20:45 +0200 blanchet killed dead code file | diff | annotate
Wed, 11 Sep 2013 09:51:30 +0200 blanchet speed up often-called function file | diff | annotate
Tue, 10 Sep 2013 15:56:51 +0200 blanchet don't be so verbose about SMT solver failures file | diff | annotate
Mon, 09 Sep 2013 23:54:59 +0200 blanchet since "full_proofs" can influence the proof search significantly (e.g. by disabling splitting for SPASS), it shouldn't be affected by the "debug" flag in the interest of minimizing confusion file | diff | annotate
Mon, 09 Sep 2013 15:22:04 +0200 blanchet limit the number of instances of a single theorem file | diff | annotate
Mon, 09 Sep 2013 15:22:04 +0200 blanchet use new monomorphizer in Sledgehammer file | diff | annotate
Thu, 22 Aug 2013 08:42:27 +0200 blanchet tuning 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 11:34:50 +0200 wenzelm more explicit sendback propertries based on mode; file | diff | annotate
Tue, 13 Aug 2013 11:34:56 +0200 blanchet added flag for jEdit/PIDE asynchronous mode file | diff | annotate
Mon, 29 Jul 2013 15:30:31 +0200 blanchet added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram") file | diff | annotate
Thu, 18 Jul 2013 20:53:22 +0200 wenzelm explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it; 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, 09 Jul 2013 18:44:59 +0200 smolkas moved code -> easier debugging file | diff | annotate
Tue, 28 May 2013 08:52:41 +0200 blanchet redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e]) file | diff | annotate
Sun, 26 May 2013 12:56:37 +0200 blanchet handle lambda-lifted problems in Isar construction code file | diff | annotate
Fri, 24 May 2013 16:43:37 +0200 blanchet improved handling of free variables' types in Isar proofs file | diff | annotate
Thu, 16 May 2013 14:58:30 +0200 blanchet correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer 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 17:43:42 +0200 blanchet renamed Sledgehammer functions with 'for' in their names to 'of' file | diff | annotate
Mon, 06 May 2013 11:03:08 +0200 smolkas added preplay tracing file | diff | annotate
Thu, 28 Mar 2013 23:44:41 +0100 boehmes new, simpler implementation of monomorphization; file | diff | annotate
Thu, 21 Feb 2013 16:36:19 +0100 blanchet tuned misleading message file | diff | annotate
Thu, 21 Feb 2013 12:22:26 +0100 blanchet generate Isar proof if Metis appears to be too slow file | diff | annotate
Wed, 20 Feb 2013 15:12:38 +0100 blanchet don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary file | diff | annotate
Wed, 20 Feb 2013 14:10:51 +0100 blanchet minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay file | diff | annotate
Wed, 20 Feb 2013 08:44:24 +0100 blanchet made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired file | diff | annotate
Tue, 19 Feb 2013 15:37:42 +0100 blanchet interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices file | diff | annotate
Mon, 18 Feb 2013 18:34:55 +0100 blanchet implement (more) accurate computation of parents file | diff | annotate
Thu, 14 Feb 2013 22:49:22 +0100 smolkas renamed sledgehammer_shrink to sledgehammer_compress file | diff | annotate
Thu, 07 Feb 2013 14:05:32 +0100 blanchet distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet also have SMT solvers alternate fact filter file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet use the right filter in each slice file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet store fact filter along with ATP slice file | diff | annotate
less more (0) -300 -100 -60 tip
isabelle