src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
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
2012-07-26 ago repaired accessibility chains generated by MaSh exporter + tuned one function out
2012-07-23 ago identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway
2012-07-23 ago distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
2012-07-23 ago tuning
2012-07-20 ago honor suggested MaSh weights
2012-07-20 ago minimal maxes + tuning
2012-07-20 ago name tuning
2012-07-20 ago fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
2012-07-18 ago optimize parent computation in MaSh + remove temporary files
2012-07-18 ago don't include hidden facts in relevance filter + tweak MaSh learning
2012-07-18 ago centrally construct expensive data structures
2012-07-18 ago more work on MaSh
2012-07-18 ago gracefully handle the case of empty theories when going up the accessibility chain
2012-07-18 ago more code rationalization in relevance filter
2012-07-11 ago moved most of MaSh exporter code to Sledgehammer
2012-07-11 ago further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)