src/HOL/Tools/reconstruction.ML
2006-01-19 ago setup: theory -> theory;
2005-09-19 ago further simplification of the Isabelle-ATP linkup
2005-05-12 ago memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
2005-04-21 ago Adapted to new interface of instantiation and unification / matching functions.
2005-04-08 ago Reconstruction code, now packaged to avoid name clashes
2005-03-07 ago Tools/meson.ML: signature, structure and "open" rather than "local"
2005-02-13 ago Deleted Library.option type.
2005-02-04 ago clausification and proof reconstruction
2005-02-03 ago new treatment of demodulation in proof reconstruction
2005-01-26 ago implemented cache for conversion to clauses
2005-01-21 ago fixed the treatment of demodulation and paramodulation
2004-12-07 ago renamed attributes to lower case
2004-12-02 ago clauses counted from 0
2004-12-02 ago new CLAUSIFY attribute for proof reconstruction with lemmas
2004-08-20 ago proof reconstruction for external ATPs