src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-03 blanchet 2014-02-03 tuning
2014-01-31 blanchet 2014-01-31 renamed many Sledgehammer ML files to clarify structure
2014-01-31 blanchet 2014-01-31 renamed ML file
2013-12-19 blanchet 2013-12-19 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-12-18 blanchet 2013-12-18 tuning
2013-12-09 blanchet 2013-12-09 disable generalization in MaSh until it is shown to help
2013-12-09 blanchet 2013-12-09 generate problems with type classes
2013-12-09 blanchet 2013-12-09 more reasonable default weight
2013-11-19 blanchet 2013-11-19 tuning
2013-11-14 blanchet 2013-11-14 have MaSh support nameless facts (i.e. proofs) and use that support
2013-10-18 blanchet 2013-10-18 make sure add: doesn't add duplicates, and works for [no_atp] facts
2013-10-17 blanchet 2013-10-17 generate a comment storing the goal nickname in "learn_prover"
2013-10-17 blanchet 2013-10-17 clarified message
2013-10-17 blanchet 2013-10-17 choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first
2013-10-17 blanchet 2013-10-17 if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"
2013-10-17 blanchet 2013-10-17 remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
2013-10-15 blanchet 2013-10-15 improved duplicate detection in "build_name_tables" by ensuring that the earliest occurrence of a duplicate (if it exists) gets picked as the canonical instance
2013-10-13 blanchet 2013-10-13 more prominent MaSh errors
2013-10-10 blanchet 2013-10-10 repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions
2013-10-10 blanchet 2013-10-10 simplify fudge factor code
2013-10-09 blanchet 2013-10-09 parallelize MeSh
2013-10-09 blanchet 2013-10-09 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
2013-10-09 blanchet 2013-10-09 optimized built-in const check
2013-10-04 blanchet 2013-10-04 more tracing
2013-10-04 blanchet 2013-10-04 more thorough spying
2013-10-04 blanchet 2013-10-04 removed pointless special case
2013-10-01 blanchet 2013-10-01 removed spurious save if nothing needs to bee learned
2013-09-24 blanchet 2013-09-24 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
2013-09-23 blanchet 2013-09-23 provide a way to override MaSh's port from configuration file
2013-09-20 blanchet 2013-09-20 reduce the number of emitted MaSh commands (among others to facilitate debugging)
2013-09-20 blanchet 2013-09-20 MaSh tweaks to facilitate debugging
2013-09-12 blanchet 2013-09-12 more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses
2013-09-12 blanchet 2013-09-12 when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
2013-09-12 blanchet 2013-09-12 minor fixes
2013-09-12 blanchet 2013-09-12 invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
2013-08-26 blanchet 2013-08-26 reverted 6c5e7143e1f6; took a better look at evaluation data this time
2013-08-26 blanchet 2013-08-26 tuned fudge factor in light of evaluation
2013-08-23 blanchet 2013-08-23 repaired num_extra_feature_facts + tuning
2013-08-23 blanchet 2013-08-23 minor MaSh fix
2013-08-23 blanchet 2013-08-23 eliminated some needless MaSh features
2013-08-23 blanchet 2013-08-23 tuned output
2013-08-23 blanchet 2013-08-23 better tracing + honor blocking better
2013-08-23 blanchet 2013-08-23 learn new facts on query if there aren't too many of them in MaSh
2013-08-22 blanchet 2013-08-22 increase relevance of unknown proximate facts
2013-08-22 blanchet 2013-08-22 fixed subtle bug with "take" + thread overlord through
2013-08-22 blanchet 2013-08-22 have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
2013-08-22 blanchet 2013-08-22 take chained and proximate facts into consideration when computing MaSh features
2013-08-22 blanchet 2013-08-22 pour extra features from proximate facts into goal, in exporter
2013-08-22 blanchet 2013-08-22 tuning
2013-08-21 blanchet 2013-08-21 improve weight computation for complex terms
2013-08-21 blanchet 2013-08-21 improved support for MaSh server
2013-08-21 blanchet 2013-08-21 get rid of some silly MaSh features
2013-08-21 blanchet 2013-08-21 weight MaSh constants by frequency
2013-08-21 blanchet 2013-08-21 only generate feature weights for queries -- they're not used elsewhere
2013-08-21 blanchet 2013-08-21 take out dangerous feature, now that all updates are permanent
2013-08-21 blanchet 2013-08-21 use new MaSh command-line arguments
2013-08-21 blanchet 2013-08-21 shutdown MaSh server
2013-08-20 blanchet 2013-08-20 adapted ML code to new version of MaSh tool