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