src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
2014-05-28 ago more generous max number of suggestions, for more safety
2014-03-21 ago more qualified names;
2014-03-15 ago more explicit treatment of verbose mode, which includes concealed entries;
2014-03-14 ago back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
2014-03-14 ago just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
2014-03-10 ago clarified Args.check_src: retain name space information for error output;
2014-03-10 ago prefer Name_Space.pretty with its builtin markup;
2014-03-06 ago tuned signature;
2014-02-03 ago tuning
2014-01-31 ago tuning
2014-01-26 ago tuned signature;
2014-01-25 ago explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
2014-01-02 ago removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)
2013-11-19 ago tuning
2013-10-18 ago make sure add: doesn't add duplicates, and works for [no_atp] facts
2013-10-17 ago no fact subsumption -- this only confuses later code, e.g. 'add:'
2013-10-15 ago drop only real duplicates, not subsumed facts -- this confuses MaSh
2013-10-09 ago normalize more equalities
2013-10-09 ago added TODO
2013-10-09 ago crank up limit a bit -- truly huge background theories are still nearly 3 times larger
2013-10-08 ago minor fact filter speedups
2013-10-08 ago more gracefully handle huge theories in relevance filters
2013-10-08 ago further optimization in relevance filter
2013-10-08 ago further speed up duplicate elimination
2013-10-08 ago more efficient theorem variable normalization
2013-10-02 ago strengthen top sort check
2013-09-24 ago encode goal digest in spying log (to detect duplicates)
2013-09-11 ago reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently
2013-09-11 ago tuning
2013-09-11 ago disable some checks for huge background theories
2013-09-11 ago tuning
2013-09-11 ago reintroduced half of f99ee3adb81d -- that part definitely looks useless (and is inefficient)
2013-09-11 ago reverted f99ee3adb81d -- that old logic seems to make a difference still today
2013-09-10 ago faster detection of tautologies
2013-09-10 ago slight speed optimization
2013-09-10 ago got rid of another slowdown factor in relevance filter
2013-09-10 ago removed completely needless, inefficient code
2013-09-10 ago minor speed optimization
2013-09-10 ago got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)
2013-09-10 ago avoid double traversal of term
2013-09-10 ago got rid of old, needless logic
2013-09-10 ago faster uniquification
2013-09-10 ago stronger fact normalization
2013-09-10 ago gracefully handle huge thys
2013-09-10 ago speed up detection of simp rules
2013-05-16 ago tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-15 ago renamed Sledgehammer functions with 'for' in their names to 'of'
2013-02-15 ago systematic conversions between nat and nibble/char;
2013-02-14 ago reform of predicate compiler / quickcheck theories:
2013-01-31 ago distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
2013-01-10 ago make name table work the way it was intended to
2013-01-06 ago put single-theorem names before multi-theorem ones (broken since 5d147d492792)
2013-01-05 ago tuned blacklisting in relevance filter
2013-01-04 ago refined class handling, to prevent cycles in fact graph
2013-01-04 ago learn from low-level, inside-class facts
2013-01-04 ago tuning
2012-12-17 ago add a timeout in induction rule instantiation
2012-12-13 ago get rid of some junk facts in the MaSh evaluation driver
2012-12-12 ago tweaked which facts are included for MaSh evaluations
2012-12-12 ago don't query blacklisted theorems in evaluation driver