src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
Sun, 03 May 2015 22:15:29 +0200 blanchet improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Fri, 03 Apr 2015 18:36:19 +0200 wenzelm tuned;
Wed, 01 Apr 2015 10:35:43 +0200 wenzelm tuned signature;
Thu, 19 Mar 2015 22:30:57 +0100 wenzelm more position information;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Sat, 24 Jan 2015 22:00:24 +0100 wenzelm tuned signature;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Thu, 06 Nov 2014 13:36:19 +0100 wenzelm prefer explicit Keyword.keywords;
Mon, 08 Sep 2014 14:04:03 +0200 blanchet never include hidden names -- these cannot be referenced afterward
Thu, 28 Aug 2014 20:05:39 +0200 blanchet gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
Mon, 18 Aug 2014 17:19:58 +0200 blanchet reordered some (co)datatype property names for more consistency
Sat, 16 Aug 2014 21:11:08 +0200 wenzelm updated to named_theorems;
Fri, 01 Aug 2014 14:43:57 +0200 blanchet whitespace tuning
Fri, 01 Aug 2014 14:43:57 +0200 blanchet remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
Fri, 01 Aug 2014 14:43:57 +0200 blanchet generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
Tue, 01 Jul 2014 16:47:10 +0200 blanchet added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
Tue, 01 Jul 2014 16:47:10 +0200 blanchet whitespace tuning
Wed, 28 May 2014 17:42:36 +0200 blanchet more generous max number of suggestions, for more safety
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Sat, 15 Mar 2014 11:22:25 +0100 wenzelm more explicit treatment of verbose mode, which includes concealed entries;
Fri, 14 Mar 2014 12:23:59 +0100 wenzelm back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
Fri, 14 Mar 2014 10:08:36 +0100 wenzelm just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
Mon, 10 Mar 2014 18:06:23 +0100 wenzelm clarified Args.check_src: retain name space information for error output;
Mon, 10 Mar 2014 15:20:41 +0100 wenzelm prefer Name_Space.pretty with its builtin markup;
Thu, 06 Mar 2014 10:12:47 +0100 wenzelm tuned signature;
Mon, 03 Feb 2014 15:33:18 +0100 blanchet tuning
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning
Sun, 26 Jan 2014 13:45:40 +0100 wenzelm tuned signature;
Sat, 25 Jan 2014 22:06:07 +0100 wenzelm explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
Thu, 02 Jan 2014 19:07:36 +0100 blanchet removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)
Tue, 19 Nov 2013 18:34:04 +0100 blanchet tuning
Fri, 18 Oct 2013 00:05:31 +0200 blanchet make sure add: doesn't add duplicates, and works for [no_atp] facts
Thu, 17 Oct 2013 23:41:00 +0200 blanchet no fact subsumption -- this only confuses later code, e.g. 'add:'
Tue, 15 Oct 2013 15:26:58 +0200 blanchet drop only real duplicates, not subsumed facts -- this confuses MaSh
Wed, 09 Oct 2013 16:38:48 +0200 blanchet normalize more equalities
Wed, 09 Oct 2013 08:28:36 +0200 blanchet added TODO
Wed, 09 Oct 2013 08:12:53 +0200 blanchet crank up limit a bit -- truly huge background theories are still nearly 3 times larger
Tue, 08 Oct 2013 21:19:46 +0200 blanchet minor fact filter speedups
Tue, 08 Oct 2013 20:56:35 +0200 blanchet more gracefully handle huge theories in relevance filters
Tue, 08 Oct 2013 16:40:03 +0200 blanchet further optimization in relevance filter
Tue, 08 Oct 2013 14:53:33 +0200 blanchet further speed up duplicate elimination
Tue, 08 Oct 2013 14:41:25 +0200 blanchet more efficient theorem variable normalization
Wed, 02 Oct 2013 22:54:42 +0200 blanchet strengthen top sort check
Tue, 24 Sep 2013 11:02:42 +0200 blanchet encode goal digest in spying log (to detect duplicates)
Wed, 11 Sep 2013 18:37:47 +0200 blanchet reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently
Wed, 11 Sep 2013 14:07:24 +0200 blanchet tuning
Wed, 11 Sep 2013 14:07:24 +0200 blanchet disable some checks for huge background theories
Wed, 11 Sep 2013 14:07:24 +0200 blanchet tuning
Wed, 11 Sep 2013 14:07:24 +0200 blanchet reintroduced half of f99ee3adb81d -- that part definitely looks useless (and is inefficient)
Wed, 11 Sep 2013 14:07:24 +0200 blanchet reverted f99ee3adb81d -- that old logic seems to make a difference still today
Tue, 10 Sep 2013 15:56:52 +0200 blanchet faster detection of tautologies
Tue, 10 Sep 2013 15:56:51 +0200 blanchet slight speed optimization
Tue, 10 Sep 2013 15:56:51 +0200 blanchet got rid of another slowdown factor in relevance filter
Tue, 10 Sep 2013 15:56:51 +0200 blanchet removed completely needless, inefficient code
Tue, 10 Sep 2013 15:56:51 +0200 blanchet minor speed optimization
Tue, 10 Sep 2013 15:56:51 +0200 blanchet got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)
Tue, 10 Sep 2013 15:56:51 +0200 blanchet avoid double traversal of term
less more (0) -100 -60 tip