src/HOL/ex/sledgehammer_tactics.ML
2011-09-02 blanchet 2011-09-02 renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
2011-08-31 blanchet 2011-08-31 more tuning
2011-08-30 nik 2011-08-30 improved handling of induction rules in Sledgehammer
2011-08-24 blanchet 2011-08-24 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
2011-08-23 blanchet 2011-08-23 clean up Sledgehammer tactic
2011-08-22 blanchet 2011-08-22 pass sound option to Sledgehammer tactic
2011-06-10 blanchet 2011-06-10 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
2011-06-06 blanchet 2011-06-06 Metis code cleanup
2011-06-06 blanchet 2011-06-06 more preparations towards hijacking Metis
2011-05-31 blanchet 2011-05-31 compile
2011-05-30 blanchet 2011-05-30 minimize with Metis if possible
2011-05-27 blanchet 2011-05-27 handle non-auto try case of Sledgehammer better
2011-05-27 blanchet 2011-05-27 fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
2011-05-22 blanchet 2011-05-22 improved Waldmeister support -- even run it by default on unit equational goals
2011-05-02 blanchet 2011-05-02 tuning
2011-05-02 blanchet 2011-05-02 have each ATP filter out dangerous facts for themselves, based on their type system
2011-05-01 blanchet 2011-05-01 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
2011-05-01 blanchet 2011-05-01 implement the new ATP type system in Sledgehammer
2011-04-21 blanchet 2011-04-21 detect some unsound proofs before showing them to the user
2011-04-21 blanchet 2011-04-21 cleanup: get rid of "may_slice" arguments without changing semantics
2011-04-21 blanchet 2011-04-21 implemented general slicing for ATPs, especially E 1.2w and above
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-24 blanchet 2011-03-24 specify proper defaults for Nitpick and Refute on TPTP + tuning
2011-03-23 blanchet 2011-03-23 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" default to "e" rather than "vampire" since E is part of the Isabelle bundle