src/HOL/TPTP/sledgehammer_tactics.ML
2016-03-28 blanchet 2016-03-28 compile
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-06 wenzelm 2014-11-06 prefer explicit Keyword.keywords (cf. 82a71046dce8);
2014-08-07 blanchet 2014-08-07 make TPTP tools work on polymorphic (TFF1) problems as well
2014-08-01 blanchet 2014-08-01 compile
2014-01-31 blanchet 2014-01-31 tuning
2014-01-31 blanchet 2014-01-31 refactor large ML file
2014-01-31 blanchet 2014-01-31 renamed ML file
2014-01-31 blanchet 2014-01-31 tuned ML file name
2013-10-17 blanchet 2013-10-17 generate a comment storing the goal nickname in "learn_prover"
2013-10-17 blanchet 2013-10-17 if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
2013-05-28 blanchet 2013-05-28 redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
2013-05-24 blanchet 2013-05-24 improved handling of free variables' types in Isar proofs
2013-05-15 blanchet 2013-05-15 renamed Sledgehammer functions with 'for' in their names to 'of'
2013-03-27 wenzelm 2013-03-27 clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;
2013-01-31 blanchet 2013-01-31 tuned data structure
2013-01-31 blanchet 2013-01-31 thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
2013-01-31 blanchet 2013-01-31 eliminated needless speed optimization -- and simplified code quite a bit
2013-01-31 blanchet 2013-01-31 distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
2013-01-31 blanchet 2013-01-31 report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
2012-11-28 smolkas 2012-11-28 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
2012-07-20 blanchet 2012-07-20 renamed ML structures
2012-07-18 blanchet 2012-07-18 centrally construct expensive data structures
2012-07-18 blanchet 2012-07-18 renamed Sledgehammer options
2012-07-18 blanchet 2012-07-18 more code rationalization in relevance filter
2012-07-18 blanchet 2012-07-18 systematize lazy names in relevance filter
2012-07-18 blanchet 2012-07-18 rationalize relevance filter, slowing moving code from Iter to MaSh
2012-07-18 blanchet 2012-07-18 killed one file
2012-07-11 blanchet 2012-07-11 further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
2012-04-27 blanchet 2012-04-27 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
2012-04-27 blanchet 2012-04-27 move file to where it belongs