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_filter.ML
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context; file | diff | annotate
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references; file | diff | annotate
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon; file | diff | annotate
Fri, 18 Mar 2011 22:55:28 +0100 blanchet added "simp:", "intro:", and "elim:" to "try" command file | diff | annotate
Thu, 17 Mar 2011 11:18:31 +0100 blanchet add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments) file | diff | annotate
Mon, 21 Feb 2011 10:31:48 +0100 blanchet give more weight to Frees than to Consts in relevance filter file | diff | annotate
Thu, 17 Feb 2011 12:14:47 +0100 blanchet export more functionality of Sledgehammer to applications (for experiments) file | diff | annotate
Wed, 16 Feb 2011 19:07:53 +0100 blanchet export useful function (needed in a Sledgehammer-related experiment) file | diff | annotate
Mon, 10 Jan 2011 15:45:46 +0100 wenzelm eliminated Int.toString; file | diff | annotate
Tue, 21 Dec 2010 04:33:17 +0100 blanchet proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; file | diff | annotate
Sun, 19 Dec 2010 13:25:18 +0100 blanchet escape backticks in altstrings file | diff | annotate
Sat, 18 Dec 2010 21:07:34 +0100 blanchet made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever); file | diff | annotate
Thu, 16 Dec 2010 15:46:54 +0100 blanchet no need to do a super-duper atomization if Metis fails afterwards anyway file | diff | annotate
Thu, 16 Dec 2010 15:12:17 +0100 blanchet reintroduce the higher penalty for skolems file | diff | annotate
Thu, 16 Dec 2010 15:12:17 +0100 blanchet comment tuning file | diff | annotate
Thu, 16 Dec 2010 15:12:17 +0100 blanchet get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts file | diff | annotate
Thu, 16 Dec 2010 15:12:17 +0100 blanchet make it more likely that induction rules are picked up by Sledgehammer file | diff | annotate
Thu, 16 Dec 2010 15:12:17 +0100 blanchet add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already file | diff | annotate
Thu, 16 Dec 2010 15:12:17 +0100 blanchet instantiate induction rules automatically file | diff | annotate
Wed, 15 Dec 2010 16:42:06 +0100 blanchet move facts supplied with "add:" to the front, so that they get a better weight (SMT) file | diff | annotate
Wed, 15 Dec 2010 12:08:41 +0100 blanchet honor "overlord" option for SMT solvers as well and don't pass "ext" to them file | diff | annotate
Wed, 15 Dec 2010 11:26:29 +0100 blanchet make Sledgehammer's relevance filter include the "ext" rule when appropriate file | diff | annotate
Wed, 15 Dec 2010 11:26:28 +0100 blanchet added Sledgehammer support for higher-order propositional reasoning file | diff | annotate
Wed, 15 Dec 2010 11:26:28 +0100 blanchet implemented partially-typed "tags" type encoding file | diff | annotate
Tue, 07 Dec 2010 16:27:07 +0100 blanchet pass constant arguments to the built-in check function, cf. d2b1fc1b8e19 file | diff | annotate
Mon, 08 Nov 2010 02:32:27 +0100 blanchet better detection of completely irrelevant facts file | diff | annotate
Sat, 06 Nov 2010 10:25:08 +0100 blanchet always honor the max relevant constraint file | diff | annotate
Fri, 05 Nov 2010 09:49:03 +0100 blanchet fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2) file | diff | annotate
Thu, 04 Nov 2010 15:31:26 +0100 blanchet pass proper type to SMT_Builtin.is_builtin file | diff | annotate
Thu, 04 Nov 2010 14:59:44 +0100 blanchet ignore facts with only theory constants in them file | diff | annotate
Thu, 04 Nov 2010 14:59:44 +0100 blanchet use the SMT integration's official list of built-ins file | diff | annotate
Fri, 29 Oct 2010 10:40:36 +0200 blanchet reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong file | diff | annotate
Thu, 28 Oct 2010 12:33:24 +0200 blanchet support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them file | diff | annotate
Tue, 26 Oct 2010 21:34:01 +0200 blanchet if "debug" is on, print list of relevant facts (poweruser request); file | diff | annotate
Tue, 26 Oct 2010 21:01:28 +0200 blanchet standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module file | diff | annotate
Tue, 26 Oct 2010 14:49:48 +0200 blanchet put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away file | diff | annotate
Fri, 22 Oct 2010 15:02:27 +0200 blanchet generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different) file | diff | annotate
Fri, 22 Oct 2010 14:47:43 +0200 blanchet replaced references with proper record that's threaded through file | diff | annotate
Tue, 05 Oct 2010 12:50:45 +0200 blanchet tuned comments file | diff | annotate
Mon, 04 Oct 2010 22:45:09 +0200 blanchet move Metis into Plain file | diff | annotate
Thu, 30 Sep 2010 20:44:53 +0200 blanchet encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions file | diff | annotate
Mon, 27 Sep 2010 09:14:39 +0200 blanchet remove needless flag file | diff | annotate
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; file | diff | annotate
Tue, 14 Sep 2010 17:23:16 +0200 blanchet tuning file | diff | annotate
Tue, 14 Sep 2010 16:34:26 +0200 blanchet handle relevance filter corner cases more gracefully; file | diff | annotate
Thu, 09 Sep 2010 18:22:04 +0200 blanchet allow Sledgehammer proofs containing nameless local facts with schematic variables in them file | diff | annotate
Thu, 09 Sep 2010 16:32:28 +0200 blanchet tuning file | diff | annotate
Thu, 02 Sep 2010 00:50:51 +0200 blanchet cosmetics file | diff | annotate
Wed, 01 Sep 2010 17:27:10 +0200 blanchet got rid of the "theory_relevant" option; file | diff | annotate
Wed, 01 Sep 2010 16:46:11 +0200 blanchet generalize theorem argument parsing syntax file | diff | annotate
Wed, 01 Sep 2010 11:59:04 +0200 blanchet fiddled with fudge factor (based on Mirabelle) file | diff | annotate
Wed, 01 Sep 2010 11:36:02 +0200 blanchet give priority to assumptions in structured proofs file | diff | annotate
Wed, 01 Sep 2010 10:26:54 +0200 blanchet introduce fudge factors to deal with "theory const" file | diff | annotate
Tue, 31 Aug 2010 23:50:59 +0200 blanchet finished renaming file | diff | annotate
Tue, 31 Aug 2010 23:46:23 +0200 blanchet shorten a few file names file | diff | annotate | base
less more (0) tip
isabelle