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
2012-12-12 ago export a pair of ML functions
2012-12-12 ago further fix related to bd9a0028b063 -- that change was per se right, but it exposed a bug in the pattern for "all"
2012-12-12 ago better tautology check -- don't reject "prod_cases3" for example
2012-12-12 ago really all facts means really all facts (well, almost)
2012-12-12 ago merge aliased theorems in MaSh dependencies, modulo symmetry of equality
2012-12-12 ago push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
2012-12-08 ago don't blacklist "case" theorems -- this causes problems in MaSh later
2012-11-26 ago tuned signature;
2012-11-12 ago fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
2012-11-12 ago avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
2012-11-12 ago centralized term printing code
2012-11-12 ago thread context correctly when printing backquoted facts
2012-10-31 ago tuning
2012-08-03 ago rule out same "technical" theories for MePo as for MaSh