src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
2013-11-20 ago support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)
2013-11-19 ago whitespace tuning
2013-11-19 ago more refactoring to accommodate SMT proofs
2013-11-19 ago tuning
2013-11-19 ago simplified old code
2013-11-19 ago refactoring
2013-11-19 ago refactoring
2013-11-19 ago refactored
2013-10-09 ago no isar proofs if preplay was not attempted
2013-09-20 ago merged "isar_try0" and "isar_minimize" options
2013-09-20 ago hardcoded obscure option
2013-09-20 ago hard-coded an obscure option
2013-09-20 ago use configuration mechanism for low-level tracing
2013-09-12 ago prefixed types and some functions with "atp_" for disambiguation
2013-08-17 ago sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
2013-08-17 ago more explicit sendback propertries based on mode;
2013-07-29 ago parse nonnumeric identifiers in E proofs correctly
2013-07-18 ago explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
2013-07-12 ago added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
2013-07-12 ago cleaner preplay interface
2013-07-12 ago minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
2013-07-11 ago optimize isar-proofs by trying different proof methods
2013-07-09 ago completely rewrote SH compress; added two parameters for experimentation/fine grained control
2013-07-09 ago moved code -> easier debugging
2013-06-26 ago tuned: cleaned up data structure
2013-06-26 ago simplified data structure
2013-06-13 ago tuning
2013-06-11 ago uncheck terms before annotation to avoid awkward syntax
2013-06-11 ago make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
2013-05-28 ago redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
2013-05-26 ago handle lambda-lifted problems in Isar construction code
2013-05-24 ago improved handling of free variables' types in Isar proofs
2013-05-20 ago parse agsyHOL proofs (as unsat cores)
2013-05-16 ago correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
2013-05-16 ago tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-15 ago renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-14 ago generate valid direct Isar proof also if the facts are contradictory
2013-05-06 ago added preplay tracing
2013-04-23 ago tuning
2013-02-23 ago make SML/NJ happy;
2013-02-21 ago generate Isar proof if Metis appears to be too slow
2013-02-20 ago ensure all conjecture clauses are in the graph -- to prevent exceptions later
2013-02-20 ago remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)
2013-02-20 ago trust preplayed proof in Mirabelle
2013-02-20 ago added case taken out by mistake
2013-02-20 ago tuning (removed redundant datatype)
2013-02-20 ago minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
2013-02-20 ago got rid of rump support for Vampire definitions
2013-02-20 ago tuning
2013-02-20 ago use new skolemizer only if some skolems have two or more arguments -- otherwise the old skolemizer cannot get the arg order wrong
2013-02-20 ago slacker comparison for Skolems, to avoid trivial equations
2013-02-20 ago made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
2013-02-19 ago avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
2013-02-18 ago split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
2013-02-18 ago simplified byline, isar_qualifier
2013-02-15 ago tuning
2013-02-15 ago repaired collateral damage from 4f0147ed8bcb
2013-02-15 ago annotate obtains with types
2013-02-15 ago made check for conjecture skolemization sound
2013-02-15 ago skolemize conjecture properly in Isar proof