src/HOL/Tools/ATP/atp_proof_reconstruct.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-13 blanchet 2014-03-13 correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
2014-02-03 blanchet 2014-02-03 merged 'reconstructors' and 'proof methods'
2014-02-02 blanchet 2014-02-02 rationalized threading of 'metis' arguments
2014-01-30 blanchet 2014-01-30 reverted unsound optimization
2014-01-30 blanchet 2014-01-30 unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer
2014-01-30 blanchet 2014-01-30 centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)
2013-12-19 blanchet 2013-12-19 pick up tfree/tvar type from SPASS-Pirate proof
2013-12-19 blanchet 2013-12-19 tuning
2013-12-19 blanchet 2013-12-19 extended ATP types with sorts
2013-12-19 blanchet 2013-12-19 removed debugging output
2013-12-19 blanchet 2013-12-19 honor SPASS-Pirate type arguments
2013-12-18 blanchet 2013-12-18 parse SPASS-Pirate types
2013-12-18 blanchet 2013-12-18 tuning
2013-12-17 blanchet 2013-12-17 tuning
2013-12-17 blanchet 2013-12-17 primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
2013-12-17 blanchet 2013-12-17 made SML/NJ happier
2013-12-16 blanchet 2013-12-16 handle Skolems gracefully for SPASS as well
2013-12-16 blanchet 2013-12-16 reverse Skolem function arguments
2013-12-16 blanchet 2013-12-16 fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
2013-12-15 blanchet 2013-12-15 use 'prop' rather than 'bool' systematically in Isar reconstruction code
2013-12-15 blanchet 2013-12-15 tuning
2013-11-19 blanchet 2013-11-19 whitespace tuning
2013-11-19 blanchet 2013-11-19 tuning
2013-11-19 blanchet 2013-11-19 more refactoring to accommodate SMT proofs
2013-11-19 blanchet 2013-11-19 simplified old code
2013-11-19 blanchet 2013-11-19 refactoring
2013-11-19 blanchet 2013-11-19 refactoring
2013-09-12 blanchet 2013-09-12 prefixed types and some functions with "atp_" for disambiguation
2013-07-29 blanchet 2013-07-29 avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference
2013-05-24 blanchet 2013-05-24 improved handling of free variables' types in Isar proofs
2013-05-16 blanchet 2013-05-16 correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-06 smolkas 2013-05-06 handle dummy atp terms
2013-02-20 blanchet 2013-02-20 slacker comparison for Skolems, to avoid trivial equations
2013-01-03 blanchet 2013-01-03 rename variable in binder, not just in body
2013-01-03 blanchet 2013-01-03 swap Vampire's Skolem arguments to bring them in line with what E and metis's new skolemizer do (helps Isar proof reconstruction in some cases)
2013-01-03 blanchet 2013-01-03 tuned comment
2013-01-02 blanchet 2013-01-02 generate "obtain" steps corresponding to skolemization inferences
2013-01-02 blanchet 2013-01-02 properly take the existential closure of skolems
2012-10-31 blanchet 2012-10-31 use metaquantification when possible in Isar proofs
2012-10-18 blanchet 2012-10-18 refactor code
2012-10-16 blanchet 2012-10-16 added proof minimization code from Steffen Smolka
2012-10-09 blanchet 2012-10-09 added type annotations to generated Isar proofs -- code by Steffen Smolka
2012-08-14 blanchet 2012-08-14 warn users about unused "using" facts
2012-07-27 blanchet 2012-07-27 extract Z3 unsat cores (for "z3_tptp")
2012-07-23 blanchet 2012-07-23 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
2012-06-26 blanchet 2012-06-26 added sorts to datastructure
2012-06-26 blanchet 2012-06-26 added type arguments to "ATerm" constructor -- but don't use them yet
2012-06-06 blanchet 2012-06-06 avoid dumping definitions several times in LEO-II proofs
2012-05-23 blanchet 2012-05-23 improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
2012-05-23 blanchet 2012-05-23 augment Satallax unsat cores with all definitions
2012-05-21 blanchet 2012-05-21 include "ext" in all Satallax proofs
2012-05-15 blanchet 2012-05-15 repair the Waldmeister endgame only for Waldmeister proofs
2012-05-14 blanchet 2012-05-14 ensure the "show" equation is not reoriented by Waldmeister
2012-05-14 blanchet 2012-05-14 ensure consistent naming of Waldmeister proof steps, so that they are not cleaned away by "clean_up_atp_proof_dependencies"
2012-05-14 blanchet 2012-05-14 graceful handling of Waldmeister endgame
2012-04-26 blanchet 2012-04-26 tuning
2012-03-27 blanchet 2012-03-27 print a hint
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;