src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
2012-12-05 ago take proximity into account for MaSh + fix a debilitating bug in feature generation
2012-12-05 ago tuning
2012-12-05 ago tweaked order of theorems to avoid forward dependencies (MaSh)
2012-12-04 ago more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
2012-12-04 ago added feature weights in MaSh
2012-12-04 ago promote local facts using a hack (for MaSh)
2012-12-04 ago turned off noisy MaSh features
2012-12-04 ago simplify MaSh term patterns + add missing global facts if there aren't too many
2012-12-04 ago MaSh improvements: deeper patterns + more respect for chained facts
2012-12-03 ago tuned names
2012-12-03 ago proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
2012-12-03 ago robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
2012-12-01 ago tuned order of functions
2012-12-01 ago proper quoting of paths in MaSh
2012-11-26 ago simplify code slightly
2012-11-26 ago moved MaSh's Python code into Isabelle
2012-11-22 ago more abstract Sendback operations, with explicit id/exec_id properties;
2012-11-12 ago thread context correctly when printing backquoted facts
2012-11-01 ago made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
2012-08-06 ago optimized saving
2012-08-03 ago remember ATP flops to avoid repeating them too quickly
2012-08-03 ago remember which MaSh proofs were found using ATPs
2012-08-03 ago rule out same "technical" theories for MePo as for MaSh
2012-08-03 ago crank up max number of dependencies
2012-08-03 ago cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
2012-07-26 ago don't export technical theorems for MaSh
2012-07-23 ago cap the number of facts returned by MaSh
2012-07-23 ago remove MaSh junk associated with size functions
2012-07-23 ago identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway
2012-07-23 ago removed MaSh junk arising from primrec definitions
2012-07-23 ago distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
2012-07-23 ago faster "save" operation
2012-07-23 ago include unknown local facts in MaSh
2012-07-23 ago ensure all calls to "mash" program are synchronous
2012-07-23 ago don't relearn old facts in Isar mode
2012-07-20 ago tune Mesh filter
2012-07-20 ago faster maximal node computation
2012-07-20 ago honor suggested MaSh weights
2012-07-20 ago relearn ATP proofs
2012-07-20 ago don't store fresh names in fact graph, since these cannot be the parents of any other facts
2012-07-20 ago cached ancestor computation
2012-07-20 ago minimal maxes + tuning
2012-07-20 ago learn from SMT proofs when they can be minimized by Metis
2012-07-20 ago clean up interesting constants a bit
2012-07-20 ago name tuning
2012-07-20 ago learning should honor the fact override and the chained facts
2012-07-20 ago fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
2012-07-20 ago added "learn_from_atp" command to MaSh, for patient users
2012-07-20 ago add versioning to MaSh state + cleanup dead code
2012-07-20 ago eliminated special handling of init case, now that "mash.py" has been optimized to handle sequences of add gracefully
2012-07-20 ago use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them
2012-07-20 ago added locality as a MaSh feature
2012-07-20 ago learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
2012-07-20 ago learn command in MaSh
2012-07-20 ago added possibility of running external MaSh commands asynchronously
2012-07-20 ago renamed ML structures
2012-07-20 ago renamed ML files