src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
2012-12-10 ago generalized notion of active area, where sendback is just one application;
2012-12-06 ago proper Sendback.markup, as required for standard Prover IDE protocol (see also c62ce309dc26);
2012-11-28 ago tweaked calculation of sledgehammer messages
2012-11-28 ago adapted sledgehammer warnings
2012-11-28 ago fixed preplaying of case splits; incorperated new name of structure: Isabelle_Markup -> Markup
2012-11-28 ago added warning when shrinking proof without preplaying
2012-11-28 ago deal with the case that metis does not time out, but fails instead
2012-11-28 ago renaming, minor tweaks, added signature
2012-11-28 ago moved thms_of_name to Sledgehammer_Util and removed copies, updated references
2012-11-28 ago removed duplicate decleration
2012-11-28 ago renamed sledgehammer_isar_reconstruct to sledgehammer_proof
2012-11-28 ago fixed problem with fact names
2012-11-28 ago remove hack and generalize code slightly
2012-11-28 ago simplified isar_qualifiers and qs merging
2012-11-28 ago put shrink in own structure
2012-11-28 ago put annotate in own structure
2012-11-28 ago support assumptions as facts for preplaying
2012-11-28 ago some minor improvements in shrink_proof
2012-11-26 ago tuned signature;
2012-11-26 ago distinguish declated tfrees from other tfrees -- only the later can be optimized away
2012-11-22 ago more abstract Sendback operations, with explicit id/exec_id properties;
2012-11-16 ago made SML/NJ happy;
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-11-06 ago renamed Sledgehammer option
2012-11-06 ago always show timing for structured proofs
2012-11-06 ago use implications rather than disjunctions to improve readability
2012-11-06 ago avoid name clashes
2012-11-06 ago fixed more "Trueprop" issues
2012-11-06 ago removed needless sort
2012-11-06 ago avoid double "Trueprop"s
2012-11-06 ago use original formulas for hypotheses and conclusion to avoid mismatches
2012-11-06 ago track formula roles in proofs and use that to determine whether the conjecture should be negated or not
2012-11-06 ago proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
2012-11-02 ago handle non-unit clauses gracefully
2012-11-02 ago several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
2012-10-31 ago fixed bool vs. prop mismatch
2012-10-31 ago took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly
2012-10-31 ago use metaquantification when possible in Isar proofs
2012-10-31 ago tuning
2012-10-19 ago made SML/NJ happy;
2012-10-18 ago tuned Isar output
2012-10-18 ago renamed Isar-proof related options + changed semantics of Isar shrinking
2012-10-18 ago tuning
2012-10-18 ago fixed theorem lookup code in Isar proof reconstruction
2012-10-18 ago tuning
2012-10-18 ago refactor code
2012-10-18 ago tuning
2012-10-16 ago added missing file
2010-10-22 ago got rid of duplicate functionality ("run_smt_solver_somehow");
2010-10-21 ago first step in adding support for an SMT backend to Sledgehammer
2010-10-05 ago hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
2010-09-25 ago make SML/NJ happy
2010-09-17 ago move functions around
2010-09-16 ago added new "Metis_Reconstruct" module, temporarily empty
2010-09-16 ago rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
2010-09-16 ago move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
2010-09-16 ago merge constructors
2010-09-16 ago factor out the inverse of "nice_atp_problem"
2010-09-16 ago use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs