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
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file file | diff | annotate
Sat, 14 Jan 2012 19:06:05 +0100 wenzelm renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const; file | diff | annotate
Mon, 02 Jan 2012 14:32:20 +0100 blanchet removed special handling for set constants in relevance filter file | diff | annotate
Sat, 24 Dec 2011 16:14:58 +0100 haftmann dropped references to obsolete facts `mem_def` and `Collect_def` file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added sorted DFG output for coming version of SPASS file | diff | annotate
Wed, 21 Sep 2011 15:55:15 +0200 blanchet tuned comment file | diff | annotate
Thu, 15 Sep 2011 10:57:40 +0200 blanchet tuning 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, 31 Aug 2011 11:52:03 +0200 blanchet more tuning file | diff | annotate
Tue, 30 Aug 2011 14:12:55 +0200 nik improved handling of induction rules in Sledgehammer file | diff | annotate
Tue, 30 Aug 2011 14:12:55 +0200 nik added generation of induction rules 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 removed unused configuration option file | diff | annotate
Mon, 27 Jun 2011 22:44:44 +0200 wenzelm merged file | diff | annotate
Mon, 27 Jun 2011 14:56:33 +0200 blanchet don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical file | diff | annotate
Mon, 27 Jun 2011 15:03:55 +0200 wenzelm old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh; file | diff | annotate
Tue, 21 Jun 2011 17:17:38 +0200 blanchet insert rather than append special facts to make it less likely that they're truncated away file | diff | annotate
Mon, 20 Jun 2011 10:41:02 +0200 blanchet respect "really_all" argument, which is used by "ATP_Export" file | diff | annotate
Thu, 16 Jun 2011 13:50:35 +0200 blanchet fixed soundness bug related to extensionality file | diff | annotate
Fri, 10 Jun 2011 12:01:15 +0200 blanchet compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time file | diff | annotate
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect; file | diff | annotate
Tue, 07 Jun 2011 14:17:35 +0200 blanchet optimized the relevance filter a little bit 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 fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet tuning -- the "appropriate" terminology is inspired from TPTP file | diff | annotate
Sun, 22 May 2011 14:51:42 +0200 blanchet improved Waldmeister support -- even run it by default on unit equational goals file | diff | annotate
Tue, 17 May 2011 15:11:36 +0200 blanchet append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism file | diff | annotate
Sun, 15 May 2011 16:40:24 +0200 wenzelm tuned signature; file | diff | annotate
Sat, 14 May 2011 21:42:17 +0200 wenzelm slightly more efficient claset operations, using Item_Net to maintain rules in canonical order; file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet remove unused parameter file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet no penality for constants that appear in chained facts file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet tune whitespace file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet added configuration options for experimental features file | diff | annotate
Thu, 05 May 2011 14:18:58 +0200 blanchet tuning file | diff | annotate
Wed, 04 May 2011 19:35:48 +0200 blanchet exploit inferred monotonicity file | diff | annotate
Tue, 03 May 2011 21:46:49 +0200 blanchet fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a file | diff | annotate
Tue, 03 May 2011 00:10:22 +0200 blanchet replaced some Unsynchronized.refs with Config.Ts file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers) file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet have each ATP filter out dangerous facts for themselves, based on their type system file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags" file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet implement the new ATP type system in Sledgehammer file | diff | annotate
Thu, 21 Apr 2011 22:18:28 +0200 blanchet detect some unsound proofs before showing them to the user file | diff | annotate
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