src/HOL/TPTP/mash_eval.ML
2012-12-16 blanchet 2012-12-16 escape nicknames
2012-12-16 blanchet 2012-12-16 generate proper nicks also for instantiated induction rules
2012-12-15 blanchet 2012-12-15 MaSh exporter can now export subsets of the facts, as consecutive ranges
2012-12-15 blanchet 2012-12-15 thread no timeout properly
2012-12-15 blanchet 2012-12-15 proper escaping in file name
2012-12-15 blanchet 2012-12-15 encode lemma name in file name
2012-12-13 blanchet 2012-12-13 use MaSh nicknames in ATP problem files to facilitate gathering of statistics
2012-12-12 blanchet 2012-12-12 merge aliased theorems in MaSh dependencies, modulo symmetry of equality
2012-12-12 blanchet 2012-12-12 better name for SMT solver files
2012-12-10 blanchet 2012-12-10 changed capitalization of MeSh filter
2012-12-10 blanchet 2012-12-10 (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
2012-12-10 blanchet 2012-12-10 have MaSh evaluator keep all raw problem/solution files in a directory
2012-12-08 blanchet 2012-12-08 don't blacklist "case" theorems -- this causes problems in MaSh later
2012-12-08 blanchet 2012-12-08 don't have MaSh pretend it knows facts it doesn't know
2012-12-08 blanchet 2012-12-08 reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo)
2012-12-08 blanchet 2012-12-08 store evaluation output in a file
2012-12-08 blanchet 2012-12-08 use parallel map
2012-12-06 blanchet 2012-12-06 use proper entry point for MaSh in test driver
2012-12-05 blanchet 2012-12-05 take proximity into account for MaSh + fix a debilitating bug in feature generation
2012-12-04 blanchet 2012-12-04 rationalized MaSh evaluation harness
2012-07-31 wenzelm 2012-07-31 made SML/NJ happy;
2012-07-26 blanchet 2012-07-26 repaired accessibility chains generated by MaSh exporter + tuned one function out
2012-07-23 blanchet 2012-07-23 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
2012-07-20 blanchet 2012-07-20 honor suggested MaSh weights
2012-07-20 blanchet 2012-07-20 relearn ATP proofs
2012-07-20 blanchet 2012-07-20 fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
2012-07-20 blanchet 2012-07-20 added "learn_from_atp" command to MaSh, for patient users
2012-07-20 blanchet 2012-07-20 renamed ML structures
2012-07-20 blanchet 2012-07-20 renamed "iter" fact filter to "MePo" (Meng--Paulson)
2012-07-20 blanchet 2012-07-20 handle local facts smoothly in MaSh
2012-07-18 blanchet 2012-07-18 repair MaSh exporter
2012-07-18 blanchet 2012-07-18 speed up tautology/metaness check
2012-07-18 blanchet 2012-07-18 learn from minimized ATP proofs
2012-07-18 blanchet 2012-07-18 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
2012-07-18 blanchet 2012-07-18 more consolidation of MaSh code
2012-07-18 blanchet 2012-07-18 drastic overhaul of MaSh data structures + fixed a few performance issues
2012-07-18 blanchet 2012-07-18 fixed order of accessibles + other tweaks to MaSh
2012-07-18 blanchet 2012-07-18 mesh facts by taking into consideration whether a fact is known to MeSh
2012-07-18 blanchet 2012-07-18 implemented meshing of Iter and MaSh results
2012-07-18 blanchet 2012-07-18 implemented MaSh QUERY operation
2012-07-18 blanchet 2012-07-18 cleaner handling of metacharacters + freshness of one-off facts
2012-07-18 blanchet 2012-07-18 improved MaSh string escaping and make more operations string-based
2012-07-18 blanchet 2012-07-18 tweak output
2012-07-18 blanchet 2012-07-18 centrally construct expensive data structures
2012-07-18 blanchet 2012-07-18 more work on MaSh
2012-07-18 blanchet 2012-07-18 renamed Sledgehammer options
2012-07-18 blanchet 2012-07-18 more code rationalization in relevance filter
2012-07-18 blanchet 2012-07-18 systematize lazy names in relevance filter
2012-07-18 blanchet 2012-07-18 renaming