src/HOL/TPTP/mash_eval.ML
2016-08-14 blanchet 2016-08-14 killed final stops in Sledgehammer and friends
2015-10-04 blanchet 2015-10-04 sped up MaSh nickname generation
2015-07-03 wenzelm 2015-07-03 clarified context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-06 wenzelm 2014-11-06 proper Keyword.keywords (cf. 82a71046dce8);
2014-09-08 blanchet 2014-09-08 added missing 'transpose'
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-07-01 blanchet 2014-07-01 clean up MaSh evaluation driver
2014-06-29 blanchet 2014-06-29 use SMT2
2014-06-29 blanchet 2014-06-29 tuning
2014-06-29 blanchet 2014-06-29 killed Python version of MaSh, now that the SML version works adequately
2014-06-27 blanchet 2014-06-27 killed dead code
2014-06-24 blanchet 2014-06-24 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
2014-06-02 blanchet 2014-06-02 add option to keep duplicates, for more precise evaluation of relevance filters
2014-05-30 blanchet 2014-05-30 added another way of invoking Python code, for experiments
2014-05-28 blanchet 2014-05-28 more generous max number of suggestions, for more safety
2014-01-31 blanchet 2014-01-31 tuning
2014-01-31 blanchet 2014-01-31 refactor large ML file
2014-01-31 blanchet 2014-01-31 renamed ML file
2014-01-31 blanchet 2014-01-31 tuned ML file name
2013-12-19 blanchet 2013-12-19 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-10-17 blanchet 2013-10-17 generate a comment storing the goal nickname in "learn_prover"
2013-09-29 wenzelm 2013-09-29 made SML/NJ happy (NB: toplevel ML environment is unmanaged);
2013-08-22 blanchet 2013-08-22 cleanup old duplicated functionality
2013-05-28 blanchet 2013-05-28 redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
2013-05-24 blanchet 2013-05-24 improved handling of free variables' types in Isar proofs
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-02-20 blanchet 2013-02-20 honor linearization option also in the evaluation driver
2013-02-19 blanchet 2013-02-19 provide two modes for MaSh driver: linearized or real visibility
2013-02-15 blanchet 2013-02-15 tuned code
2013-02-15 blanchet 2013-02-15 more MaSh tracing
2013-02-07 blanchet 2013-02-07 more robustness w.r.t. 0
2013-01-31 blanchet 2013-01-31 compile
2013-01-31 blanchet 2013-01-31 more precise output of selected facts
2013-01-31 blanchet 2013-01-31 distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
2013-01-18 blanchet 2013-01-18 optimization -- evaluate conversion to table only once
2013-01-17 blanchet 2013-01-17 use correct weights in MeSh driver
2013-01-17 blanchet 2013-01-17 use precomputed MaSh/MePo data whenever available
2013-01-17 blanchet 2013-01-17 provide a means to skip a method
2013-01-17 blanchet 2013-01-17 evaluate more cases (cf. paper)
2013-01-11 blanchet 2013-01-11 start using MaSh hints
2013-01-11 blanchet 2013-01-11 always compare theorem using the same, weaker function
2013-01-10 blanchet 2013-01-10 export MeSh data as well
2013-01-08 blanchet 2013-01-08 tuned output
2013-01-06 blanchet 2013-01-06 also generate queries for goals with too many Isar dependencies
2013-01-04 blanchet 2013-01-04 refined class handling, to prevent cycles in fact graph
2012-12-28 blanchet 2012-12-28 tuned ML function name
2012-12-27 blanchet 2012-12-27 improved thm order hack, in case the default names are overridden
2012-12-27 blanchet 2012-12-27 fixed total
2012-12-18 blanchet 2012-12-18 avoid references altogether
2012-12-18 blanchet 2012-12-18 no need for tracing
2012-12-17 blanchet 2012-12-17 synchronize access to shared reference and print proper total
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