src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
2014-06-02 ago add option to keep duplicates, for more precise evaluation of relevance filters
2014-05-30 ago made 'Kuehlwein-style' be really like Python code, we now think
2014-05-30 ago make SML code closer to Python code when 'nb_kuehlwein_style' is true
2014-05-30 ago added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
2014-05-30 ago added another way of invoking Python code, for experiments
2014-05-30 ago make SML naive Bayes closer to Python version
2014-05-30 ago more work on exporter
2014-05-30 ago extend exporter with new versions of MaSh
2014-05-28 ago more generous max number of suggestions, for more safety
2014-05-28 ago changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
2014-05-28 ago export more ML functions, for experimentation
2014-05-28 ago disabled IDF for now -- empirical evidence points the wrong way (as usual)
2014-05-28 ago tuning
2014-05-28 ago tuning
2014-05-28 ago optimized computation
2014-05-28 ago enabled IDF for naive Bayes ML
2014-05-28 ago tuning
2014-05-28 ago repaired subscript problem in SML kNN
2014-05-28 ago tuning
2014-05-28 ago always remove duplicates in meshing + use weights for Naive Bayes
2014-05-27 ago updated naive Bayes
2014-05-26 ago renamed 'MaSh' option
2014-05-23 ago automatically reload state file when it changes on disk
2014-05-22 ago avoid slow inspection of proof terms now that dependencies are stored in 'state'
2014-05-22 ago properly mark relearns as dirty
2014-05-22 ago disable weights that cause more harm than they help in kNN
2014-05-22 ago add self dependency to naive Bayes
2014-05-22 ago make MaSh Python the default when passing 'fact_filter = mash' without enabling the 'maSh' Isabelle system option
2014-05-22 ago reverted '|' features in MaSh -- these sounded like a good idea but never really worked
2014-05-22 ago until naive Bayes supports weights, don't incorporate 'extra' low-weight features
2014-05-21 ago added comment
2014-05-20 ago added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
2014-05-20 ago added Isabelle system option 'mash'
2014-05-20 ago more flexible environment variable
2014-05-20 ago tuning
2014-05-20 ago implemented MaSh/SML hints
2014-05-20 ago better way to take invisible facts into account than 'island' business
2014-05-20 ago cleaner handling of learned proofs
2014-05-20 ago implemented learning of single proofs in SML MaSh
2014-05-19 ago take weights into consideration in knn
2014-05-19 ago added SML implementation of MaSh
2014-05-19 ago started work on MaSh/SML
2014-05-19 ago tune
2014-05-19 ago store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
2014-05-19 ago hide more consts to beautify documentation
2014-03-27 ago clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-22 ago more antiquotations;
2014-02-21 ago adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-03 ago tuning
2014-01-31 ago renamed many Sledgehammer ML files to clarify structure
2014-01-31 ago renamed ML file
2013-12-19 ago made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-12-18 ago tuning
2013-12-09 ago disable generalization in MaSh until it is shown to help
2013-12-09 ago generate problems with type classes
2013-12-09 ago more reasonable default weight
2013-11-19 ago tuning
2013-11-14 ago have MaSh support nameless facts (i.e. proofs) and use that support
2013-10-18 ago make sure add: doesn't add duplicates, and works for [no_atp] facts
2013-10-17 ago generate a comment storing the goal nickname in "learn_prover"