src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
2016-04-02 ago prefer infix operations;
2016-02-01 ago avoid error in Isar proof reconstruction if no ATP proof is available
2015-06-29 ago removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
2015-03-03 ago SPASS-Pirate is now called Pirate
2014-10-31 ago discontinued obsolete Output.urgent_message;
2014-10-12 ago improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
2014-10-02 ago more precise lemma insertion
2014-10-02 ago insert lemmas closer to where they are needed, both for esthetics and (primarily) for correctness in case the lemma refers to a skolem
2014-10-02 ago eliminate duplicate hypotheses (which can arise due to (un)clausification)
2014-10-02 ago 'moura' method is also useful for reconstructing skolemization of lambda-lifting of formulas for other provers than Z3
2014-09-15 ago tuning
2014-09-15 ago removed accidental '@{print}'
2014-09-02 ago Some work on the new waldmeister integration
2014-08-28 ago renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
2014-08-28 ago removed show stuttering
2014-08-28 ago try 'skolem' method first for Z3
2014-08-28 ago added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
2014-08-28 ago renamed new SMT module from 'SMT2' to 'SMT'
2014-08-05 ago rationalize Skolem names
2014-08-05 ago tuning
2014-08-05 ago tuning
2014-08-04 ago deal with E definitions
2014-08-04 ago cleaner 'compress' option
2014-08-04 ago tuned terminology (cf. 'isar_proofs' option)
2014-08-04 ago rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
2014-08-02 ago better duplicate detection
2014-08-01 ago normalize conjectures vs. negated conjectures when comparing terms
2014-08-01 ago tweaked 'clone' formula detection
2014-08-01 ago fine-tuned Isar reconstruction, esp. boolean simplifications
2014-08-01 ago centralized boolean simplification so that e.g. LEO-II benefits from it
2014-08-01 ago better handling of variable names
2014-08-01 ago nicer generated variable names
2014-08-01 ago tuning
2014-08-01 ago tuning
2014-08-01 ago more precise handling of LEO-II skolemization
2014-08-01 ago beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
2014-08-01 ago added appropriate method for skolemization of Z3 steps to the mix
2014-08-01 ago tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
2014-08-01 ago tuning
2014-08-01 ago eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
2014-07-30 ago Skolemization for tmp_ite_elim rule in the SMT solver veriT.
2014-07-30 ago Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
2014-07-30 ago Whitespace and indentation correction.
2014-07-30 ago imported patch hilbert_choice_support
2014-07-30 ago veriT changes for lifted terms, and ite_elim rules.
2014-07-30 ago Subproofs for the SMT solver veriT.
2014-07-30 ago Basic support for the SMT prover veriT.
2014-07-30 ago Skolemization support for leo-II and Zipperposition.
2014-07-30 ago also try 'metis' with 'full_types'
2014-07-24 ago refined filter for ATP steps to avoid 'have True' steps in E proofs
2014-07-24 ago 'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
2014-06-24 ago supports gradual skolemization (cf. Z3) by threading context through correctly
2014-06-24 ago given two one-liners, only show the best of the two
2014-06-24 ago don't generate Isar proof skeleton for what amounts to a one-line proof
2014-06-12 ago renamed Sledgehammer options
2014-06-02 ago basic setup for zipperposition prover
2014-05-22 ago properly reconstruct helpers in Z3 proofs
2014-05-22 ago tuning
2014-05-16 ago correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
2014-05-16 ago use 'simp add:' syntax in Sledgehammer rather than 'using'