src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
2010-06-02 blanchet 2010-06-02 handle Vampire's definitions smoothly
2010-06-02 blanchet 2010-06-02 fix bug in direct Isar proofs, which was exhibited by the "BigO" example
2010-06-02 blanchet 2010-06-02 show types in Isar proofs, but not for free variables; this makes proofs more robust, without as much clutter as there used to be when types were enabled previously
2010-05-28 blanchet 2010-05-28 merged
2010-05-28 blanchet 2010-05-28 make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-17 blanchet 2010-05-17 make sure chained facts don't pop up in the metis proof
2010-05-17 blanchet 2010-05-17 fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
2010-05-14 blanchet 2010-05-14 renamed options
2010-05-14 blanchet 2010-05-14 made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code
2010-05-01 krauss 2010-05-01 made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
2010-05-01 krauss 2010-05-01 Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)
2010-05-01 blanchet 2010-05-01 now if this doesn't make SML/NJ happy, nothing will
2010-04-30 blanchet 2010-04-30 eliminate trivial case splits from Isar proofs
2010-04-30 blanchet 2010-04-30 identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
2010-04-29 blanchet 2010-04-29 uncomment code
2010-04-29 blanchet 2010-04-29 be more discriminate: some one-line Isar proofs are silly
2010-04-29 blanchet 2010-04-29 one-step Isar proofs are not always pointless
2010-04-29 blanchet 2010-04-29 the SPASS output syntax is more general than I thought -- such a pity that there's no documentation
2010-04-29 blanchet 2010-04-29 fixed definition of "bad frees" so that it actually works
2010-04-29 blanchet 2010-04-29 don't remove last line of proof
2010-04-29 blanchet 2010-04-29 handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
2010-04-29 blanchet 2010-04-29 make SML/NJ happy, take 2
2010-04-29 blanchet 2010-04-29 use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
2010-04-29 blanchet 2010-04-29 expand combinators in Isar proofs constructed by Sledgehammer; this requires shuffling around a couple of functions previously defined in Refute
2010-04-28 blanchet 2010-04-28 improve unskolemization
2010-04-28 blanchet 2010-04-28 try out Vampire 11 and parse its output correctly; will revert to Vampire 9 if 11 doesn't perform as well
2010-04-28 blanchet 2010-04-28 save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
2010-04-28 blanchet 2010-04-28 unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
2010-04-28 blanchet 2010-04-28 remove Sledgehammer's "sorts" option to annotate variables with sorts in proof; what we need is smarter type annotations for variables _and_ constants
2010-04-28 blanchet 2010-04-28 support Vampire definitions of constants as "let" constructs in Isar proofs
2010-04-27 blanchet 2010-04-27 tuning
2010-04-27 blanchet 2010-04-27 polish Isar proofs: don't mention facts twice, and don't show one-liner "structured" proofs
2010-04-27 blanchet 2010-04-27 reintroduce missing "gen_all_vars" call
2010-04-27 blanchet 2010-04-27 fix types of "fix" variables to help proof reconstruction and aid readability
2010-04-27 blanchet 2010-04-27 allow schematic variables in types in terms that are reconstructed by Sledgehammer
2010-04-27 blanchet 2010-04-27 new Isar proof construction code: stringfy axiom names correctly
2010-04-27 blanchet 2010-04-27 honor "shrink_proof" Sledgehammer option
2010-04-27 blanchet 2010-04-27 fix SML/NJ compilation (I hope)
2010-04-26 blanchet 2010-04-26 make compile (and not just load dynamically)
2010-04-26 blanchet 2010-04-26 introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method; the code is still somewhat experimental but any exceptions it throws are catched, and Sledgehammer will still yield a one-line metis proof in case of proof reconstruction failure
2010-04-25 blanchet 2010-04-25 cosmetics
2010-04-25 blanchet 2010-04-25 cosmetics
2010-04-25 blanchet 2010-04-25 support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-25 blanchet 2010-04-25 cosmetics: rename internal functions
2010-04-23 blanchet 2010-04-23 handle ATP proof delimiters in a cleaner, more extensible fashion
2010-04-23 blanchet 2010-04-23 handle SPASS's equality predicate correctly in Isar proof reconstruction
2010-04-23 blanchet 2010-04-23 added Isar proof reconstruction support for SPASS -- which means all provers can now yield Isar proofs; the implementation might still be flaky, but exceptions are caught so that a proof reconstruction failure doesn't result in a Sledgehammer failure (the one-line Metis proof might still work after all)
2010-04-22 blanchet 2010-04-22 minor code cleanup
2010-04-22 blanchet 2010-04-22 if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
2010-04-22 blanchet 2010-04-22 Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes; this solves the unification exception that consistently was thrown for Cezary's "FSet3" theory
2010-04-21 blanchet 2010-04-21 failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is
2010-04-21 blanchet 2010-04-21 pass relevant options from "sledgehammer" to "sledgehammer minimize"; one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files
2010-04-19 blanchet 2010-04-19 get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
2010-04-19 blanchet 2010-04-19 cosmetics
2010-04-19 blanchet 2010-04-19 make Sledgehammer's minimizer also minimize Isar proofs
2010-04-14 blanchet 2010-04-14 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu; and added "atp" as alias for "atps"
2010-04-01 blanchet 2010-04-01 fixed layout of Sledgehammer output
2010-03-29 blanchet 2010-03-29 added "modulus" and "sorts" options to control Sledgehammer's Isar proof output