src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
2011-04-21 blanchet 2011-04-21 detect some unsound proofs before showing them to the user
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-03-18 blanchet 2011-03-18 added "simp:", "intro:", and "elim:" to "try" command
2011-03-17 blanchet 2011-03-17 add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments)
2011-02-21 blanchet 2011-02-21 give more weight to Frees than to Consts in relevance filter
2011-02-17 blanchet 2011-02-17 export more functionality of Sledgehammer to applications (for experiments)
2011-02-16 blanchet 2011-02-16 export useful function (needed in a Sledgehammer-related experiment)
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2010-12-21 blanchet 2010-12-21 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction
2010-12-19 blanchet 2010-12-19 escape backticks in altstrings
2010-12-18 blanchet 2010-12-18 made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever); disabled inductions (E and SPASS don't like them), but kept "ext" (seems more harmless)
2010-12-16 blanchet 2010-12-16 no need to do a super-duper atomization if Metis fails afterwards anyway
2010-12-16 blanchet 2010-12-16 reintroduce the higher penalty for skolems
2010-12-16 blanchet 2010-12-16 comment tuning
2010-12-16 blanchet 2010-12-16 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
2010-12-16 blanchet 2010-12-16 make it more likely that induction rules are picked up by Sledgehammer
2010-12-16 blanchet 2010-12-16 add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
2010-12-16 blanchet 2010-12-16 instantiate induction rules automatically
2010-12-15 blanchet 2010-12-15 move facts supplied with "add:" to the front, so that they get a better weight (SMT)
2010-12-15 blanchet 2010-12-15 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
2010-12-15 blanchet 2010-12-15 make Sledgehammer's relevance filter include the "ext" rule when appropriate
2010-12-15 blanchet 2010-12-15 added Sledgehammer support for higher-order propositional reasoning
2010-12-15 blanchet 2010-12-15 implemented partially-typed "tags" type encoding
2010-12-07 blanchet 2010-12-07 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
2010-11-08 blanchet 2010-11-08 better detection of completely irrelevant facts
2010-11-06 blanchet 2010-11-06 always honor the max relevant constraint
2010-11-05 blanchet 2010-11-05 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
2010-11-04 blanchet 2010-11-04 pass proper type to SMT_Builtin.is_builtin
2010-11-04 blanchet 2010-11-04 ignore facts with only theory constants in them
2010-11-04 blanchet 2010-11-04 use the SMT integration's official list of built-ins
2010-10-29 blanchet 2010-10-29 reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong
2010-10-28 blanchet 2010-10-28 support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
2010-10-26 blanchet 2010-10-26 if "debug" is on, print list of relevant facts (poweruser request); internal renaming
2010-10-26 blanchet 2010-10-26 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
2010-10-26 blanchet 2010-10-26 put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
2010-10-22 blanchet 2010-10-22 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
2010-10-22 blanchet 2010-10-22 replaced references with proper record that's threaded through
2010-10-05 blanchet 2010-10-05 tuned comments
2010-10-04 blanchet 2010-10-04 move Metis into Plain
2010-09-30 blanchet 2010-09-30 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
2010-09-27 blanchet 2010-09-27 remove needless flag
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-14 blanchet 2010-09-14 tuning
2010-09-14 blanchet 2010-09-14 handle relevance filter corner cases more gracefully; e.g. the minimizer selects 15 facts but "max_relevant = 14"
2010-09-09 blanchet 2010-09-09 allow Sledgehammer proofs containing nameless local facts with schematic variables in them
2010-09-09 blanchet 2010-09-09 tuning
2010-09-02 blanchet 2010-09-02 cosmetics
2010-09-01 blanchet 2010-09-01 got rid of the "theory_relevant" option; instead, have fudge factors that behave more smoothly for all provers
2010-09-01 blanchet 2010-09-01 generalize theorem argument parsing syntax
2010-09-01 blanchet 2010-09-01 fiddled with fudge factor (based on Mirabelle)
2010-09-01 blanchet 2010-09-01 give priority to assumptions in structured proofs
2010-09-01 blanchet 2010-09-01 introduce fudge factors to deal with "theory const"
2010-08-31 blanchet 2010-08-31 finished renaming
2010-08-31 blanchet 2010-08-31 shorten a few file names