src/HOL/TPTP/mash_eval.ML
2012-12-05 ago take proximity into account for MaSh + fix a debilitating bug in feature generation
2012-12-04 ago rationalized MaSh evaluation harness
2012-07-31 ago made SML/NJ happy;
2012-07-26 ago repaired accessibility chains generated by MaSh exporter + tuned one function out
2012-07-23 ago distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
2012-07-20 ago honor suggested MaSh weights
2012-07-20 ago relearn ATP proofs
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 renamed ML structures
2012-07-20 ago renamed "iter" fact filter to "MePo" (Meng--Paulson)
2012-07-20 ago handle local facts smoothly in MaSh
2012-07-18 ago repair MaSh exporter
2012-07-18 ago speed up tautology/metaness check
2012-07-18 ago learn from minimized ATP proofs
2012-07-18 ago improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
2012-07-18 ago more consolidation of MaSh code
2012-07-18 ago drastic overhaul of MaSh data structures + fixed a few performance issues
2012-07-18 ago fixed order of accessibles + other tweaks to MaSh
2012-07-18 ago mesh facts by taking into consideration whether a fact is known to MeSh
2012-07-18 ago implemented meshing of Iter and MaSh results
2012-07-18 ago implemented MaSh QUERY operation
2012-07-18 ago cleaner handling of metacharacters + freshness of one-off facts
2012-07-18 ago improved MaSh string escaping and make more operations string-based
2012-07-18 ago tweak output
2012-07-18 ago centrally construct expensive data structures
2012-07-18 ago more work on MaSh
2012-07-18 ago renamed Sledgehammer options
2012-07-18 ago more code rationalization in relevance filter
2012-07-18 ago systematize lazy names in relevance filter
2012-07-18 ago renaming