src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
2016-04-02 ago prefer infix operations;
2016-03-28 ago early warning when Sledgehammer finds a proof
2016-03-03 ago clarified modules;
2015-11-30 ago removed tracing
2015-11-16 ago more tracing in MaSh
2015-10-04 ago speed up MaSh duplicate check
2015-10-04 ago sped up MaSh nickname generation
2015-10-03 ago speed up MaSh
2015-10-02 ago further reduced dependency on legacy async thread manager
2015-08-28 ago eliminated obsolete environment variable
2015-08-18 ago proper platform_path;
2015-08-16 ago prefer theory_id operations;
2015-07-05 ago more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;
2015-07-03 ago clarified context;
2015-07-03 ago tuned signature;
2015-07-03 ago tuned signature;
2015-04-01 ago tuned signature;
2015-03-31 ago more standard Long_Name operations;
2015-03-31 ago tuned;
2015-03-06 ago Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 ago tuned signature -- prefer qualified names;
2015-02-06 ago careful about visibility of facts that have the same 'theory' in optimization
2015-02-02 ago less confusing constant
2015-02-02 ago tuning
2015-01-29 ago more explicit indication of Async_Manager_Legacy as Proof General legacy;
2014-12-22 ago separate module Random;
2014-11-26 ago renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-06 ago prefer explicit Keyword.keywords;
2014-10-31 ago discontinued obsolete Output.urgent_message;
2014-08-01 ago tuning
2014-08-01 ago eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
2014-07-24 ago don't needlessly regenerate entire file when the time stamps are equal
2014-07-24 ago eliminated source of 'DUP's in MaSh
2014-07-24 ago fixed sorting (broken since 9cc802a8ab06)
2014-07-24 ago beware of duplicate fact names
2014-07-19 ago made SML/NJ happier
2014-07-15 ago made SML/NJ happier
2014-07-15 ago record MaSh algorithm in spying data
2014-07-15 ago also learn when 'fact_filter =' is set explicitly
2014-07-15 ago no warning in case MaSh is disabled
2014-07-15 ago no need for 'mash' subdirectory after removal of Python program
2014-07-12 ago tuning
2014-07-12 ago made SML/NJ happier
2014-07-09 ago tuned terminology
2014-07-09 ago improvements to the machine learning algos (due to Cezary K.)
2014-07-01 ago changed default MaSh engine
2014-07-01 ago removed needless code
2014-07-01 ago speed up MaSh a bit
2014-07-01 ago mix NB and kNN
2014-07-01 ago tuned (reordered) code
2014-06-29 ago tuning
2014-06-29 ago killed Python version of MaSh, now that the SML version works adequately
2014-06-27 ago correctly take weights into consideration
2014-06-27 ago use right theory name for theorems in evaluation driver
2014-06-27 ago killed dead code
2014-06-27 ago reintroduced 'extra features' + only print message in verbose mode
2014-06-27 ago got rid of hard-coded weights, now that we have TFIDF
2014-06-27 ago tuning
2014-06-27 ago tuning
2014-06-27 ago reintroduced 'extra features' but with lower weight than before (to account for tfidf)