src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
2016-04-02 ago prefer infix operations;
2015-10-15 ago removed too aggressive underscorization
2015-10-05 ago further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
2015-03-04 ago tuned signature -- prefer qualified names;
2015-01-24 ago tuned signature;
2015-01-24 ago tuned message;
2014-11-26 ago renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-11-06 ago prefer explicit Keyword.keywords;
2014-11-05 ago eliminated pointless dynamic keywords (TTY legacy);
2014-11-05 ago explicit type Keyword.keywords;
2014-11-01 ago recover via scanner;
2014-11-01 ago simplified -- scanning is never interactive;
2014-10-08 ago added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-08-21 ago tuned signature -- define some elementary operations earlier;
2014-08-10 ago merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
2014-08-01 ago careful when calling 'Thm.proof_body_of' -- it can throw exceptions
2014-08-01 ago peek instead of joining -- is perhaps less risky
2014-08-01 ago generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
2014-06-24 ago optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
2014-05-28 ago more generous max number of suggestions, for more safety
2014-05-22 ago reverted '|' features in MaSh -- these sounded like a good idea but never really worked
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)