src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
2014-06-02 ago tuned whitespace
2014-03-21 ago more qualified names;
2014-02-03 ago tuning
2014-01-31 ago renamed ML file
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-17 ago fast track -- avoid domain error in 0 case
2013-10-15 ago drop only real duplicates, not subsumed facts -- this confuses MaSh
2013-10-10 ago simplify fudge factor code
2013-10-09 ago run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
2013-10-09 ago use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
2013-10-09 ago minor performance tuning
2013-10-09 ago use plain types instead of dedicated type pattern
2013-10-09 ago duplicate term and type patterns
2013-09-11 ago killed dead code
2013-09-11 ago get rid of another complication in relevance filter
2013-09-11 ago renamed config option
2013-09-11 ago kick out totally hopeless facts after 5 iterations to speed things up
2013-09-11 ago got rid of currently unused data structure, to speed up relevance filter
2013-09-09 ago make facts like "mem_Collect_eq" more likely to be picked up by few-fact slices
2013-08-23 ago thread information about when a constant became relevant through MePo -- the information is not used yet but could help fight starvation in the (ITP) world
2013-08-21 ago weight MaSh constants by frequency
2013-05-15 ago renamed Sledgehammer functions with 'for' in their names to 'of'
2013-02-07 ago tuned indent
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-19 ago tuning
2012-12-20 ago better weight functions for MePo/MaSh etc.
2012-12-05 ago take proximity into account for MaSh + fix a debilitating bug in feature generation
2012-12-05 ago tuning
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-07-20 ago tune Mesh filter
2012-07-20 ago honor suggested MaSh weights
2012-07-20 ago renamed ML structures
2012-07-20 ago renamed ML files