src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
2014-02-03 ago merged 'reconstructors' and 'proof methods'
2014-01-31 ago generalized preplaying infrastructure to store various results for various methods
2014-01-31 ago tuning
2013-12-19 ago tuning
2013-12-19 ago made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-12-09 ago generate problems with type classes
2013-10-15 ago made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
2013-10-04 ago more Sledgehammer spying -- record fact indices
2013-09-24 ago encode goal digest in spying log (to detect duplicates)
2013-09-23 ago added "spy" option to Sledgehammer
2013-07-12 ago removed |>! and #>!
2013-07-12 ago added |>! and #>! for convenient printing of timing information
2013-07-09 ago completely rewrote SH compress; added two parameters for experimentation/fine grained control
2013-05-11 ago prefer explicitly qualified exceptions, which is particular important for robust handlers;
2013-02-18 ago implement (more) accurate computation of parents
2013-01-31 ago tuned data structure
2013-01-31 ago thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
2013-01-04 ago refined class handling, to prevent cycles in fact graph
2013-01-04 ago learn from low-level, inside-class facts
2012-12-20 ago better weight functions for MePo/MaSh etc.
2012-12-15 ago thread no timeout properly
2012-12-12 ago merge aliased theorems in MaSh dependencies, modulo symmetry of equality
2012-11-28 ago moved thms_of_name to Sledgehammer_Util and removed copies, updated references
2012-11-12 ago avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
2012-11-12 ago centralized term printing code
2012-08-03 ago cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
2012-07-20 ago added "learn_from_atp" command to MaSh, for patient users
2012-07-20 ago learn command in MaSh
2012-07-18 ago more consolidation of MaSh code
2012-07-18 ago drastic overhaul of MaSh data structures + fixed a few performance issues
2012-07-18 ago more code rationalization in relevance filter
2012-07-11 ago moved most of MaSh exporter code to Sledgehammer
2012-03-16 ago clarified Keyword.is_keyword: union of minor and major;
2011-05-31 ago first step in sharing more code between ATP and Metis translation
2011-05-29 ago normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
2011-05-27 ago try both "metis" and (on failure) "metisFT" in replay
2011-05-27 ago show time taken for reconstruction
2011-05-27 ago use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
2011-05-27 ago merge timeout messages from several ATPs into one message to avoid clutter
2011-05-27 ago fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
2011-05-24 ago eliminated more code duplication in Nitrox
2011-05-22 ago improved Waldmeister support -- even run it by default on unit equational goals
2011-05-20 ago improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
2011-05-20 ago reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts
2011-05-12 ago improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
2011-05-05 ago query typedefs as well for monotonicity
2011-05-04 ago exploit inferred monotonicity
2011-04-08 ago discontinued special treatment of structure Lexicon;
2010-12-16 ago no need to do a super-duper atomization if Metis fails afterwards anyway
2010-12-16 ago instantiate induction rules automatically
2010-11-20 ago renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-03 ago standardize on seconds for Nitpick and Sledgehammer timeouts
2010-09-29 ago finished renaming file and module
2010-09-27 ago rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
2010-09-20 ago added XML.content_of convenience -- cover XML.body, which is the general situation;
2010-09-17 ago move functions around
2010-09-16 ago avoid code duplication
2010-09-14 ago speed up helper function
2010-09-11 ago implemented Auto Sledgehammer
2010-08-26 ago improve SPASS hack, when a clause comes from several facts