src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-06 blanchet 2015-02-06 careful about visibility of facts that have the same 'theory' in optimization
2015-02-02 blanchet 2015-02-02 less confusing constant
2015-02-02 blanchet 2015-02-02 tuning
2015-01-29 wenzelm 2015-01-29 more explicit indication of Async_Manager_Legacy as Proof General legacy;
2014-12-22 wenzelm 2014-12-22 separate module Random; proper Synchronized.var;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-06 wenzelm 2014-11-06 prefer explicit Keyword.keywords;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-08-01 blanchet 2014-08-01 tuning
2014-08-01 blanchet 2014-08-01 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
2014-07-24 blanchet 2014-07-24 don't needlessly regenerate entire file when the time stamps are equal
2014-07-24 blanchet 2014-07-24 eliminated source of 'DUP's in MaSh
2014-07-24 blanchet 2014-07-24 fixed sorting (broken since 9cc802a8ab06)
2014-07-24 blanchet 2014-07-24 beware of duplicate fact names
2014-07-19 blanchet 2014-07-19 made SML/NJ happier
2014-07-15 blanchet 2014-07-15 made SML/NJ happier
2014-07-15 blanchet 2014-07-15 record MaSh algorithm in spying data
2014-07-15 blanchet 2014-07-15 also learn when 'fact_filter =' is set explicitly
2014-07-15 blanchet 2014-07-15 no warning in case MaSh is disabled
2014-07-15 blanchet 2014-07-15 no need for 'mash' subdirectory after removal of Python program
2014-07-12 blanchet 2014-07-12 tuning
2014-07-12 blanchet 2014-07-12 made SML/NJ happier
2014-07-09 blanchet 2014-07-09 tuned terminology
2014-07-09 blanchet 2014-07-09 improvements to the machine learning algos (due to Cezary K.)
2014-07-01 blanchet 2014-07-01 changed default MaSh engine
2014-07-01 blanchet 2014-07-01 removed needless code
2014-07-01 blanchet 2014-07-01 speed up MaSh a bit
2014-07-01 blanchet 2014-07-01 mix NB and kNN
2014-07-01 blanchet 2014-07-01 tuned (reordered) code
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 correctly take weights into consideration
2014-06-27 blanchet 2014-06-27 use right theory name for theorems in evaluation driver
2014-06-27 blanchet 2014-06-27 killed dead code
2014-06-27 blanchet 2014-06-27 reintroduced 'extra features' + only print message in verbose mode
2014-06-27 blanchet 2014-06-27 got rid of hard-coded weights, now that we have TFIDF
2014-06-27 blanchet 2014-06-27 tuning
2014-06-27 blanchet 2014-06-27 tuning
2014-06-27 blanchet 2014-06-27 reintroduced 'extra features' but with lower weight than before (to account for tfidf)
2014-06-26 blanchet 2014-06-26 reintroduced MaSh hints, this time as persistent creatures
2014-06-26 blanchet 2014-06-26 always expand all paths
2014-06-26 blanchet 2014-06-26 tuned output
2014-06-26 blanchet 2014-06-26 tuned output
2014-06-26 blanchet 2014-06-26 right array indexing
2014-06-26 blanchet 2014-06-26 incremental learning when learing several facts
2014-06-26 blanchet 2014-06-26 tuning
2014-06-26 blanchet 2014-06-26 more incremental learning of single fact
2014-06-26 blanchet 2014-06-26 avoid needless (trivial) reordering on load
2014-06-26 blanchet 2014-06-26 recompute learning data at learning time, not query time
2014-06-26 blanchet 2014-06-26 imported patch killed_num_known_facts0
2014-06-26 blanchet 2014-06-26 refactoring
2014-06-26 blanchet 2014-06-26 renamed experimental learning engines
2014-06-26 blanchet 2014-06-26 tuning
2014-06-26 blanchet 2014-06-26 refactoring
2014-06-26 blanchet 2014-06-26 removed experimental machine learning engine
2014-06-26 blanchet 2014-06-26 store string-to-index tables in memory
2014-06-26 blanchet 2014-06-26 disable 'extra' feature tainting for now
2014-06-26 blanchet 2014-06-26 tuning