src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
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)