src/HOL/Reconstruction.thy
2006-06-04 mengj 2006-06-04 Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
2006-01-27 mengj 2006-01-27 Added new file Tools/ATP/reduce_axiomsN.ML
2005-12-21 paulson 2005-12-21 new hash table module in HOL/Too/s
2005-10-28 mengj 2005-10-28 Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
2005-10-14 paulson 2005-10-14 deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-10 paulson 2005-10-10 small tidy-up of utility functions
2005-09-23 webertj 2005-09-23 spaces inserted in header
2005-09-20 wenzelm 2005-09-20 tuned theory dependencies;
2005-09-19 paulson 2005-09-19 further simplification of the Isabelle-ATP linkup
2005-09-19 paulson 2005-09-19 simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-17 wenzelm 2005-09-17 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
2005-09-15 paulson 2005-09-15 moving Commutative_Ring to the correct theory
2005-09-08 paulson 2005-09-08 consolidation of duplicate code in Isabelle-ATP linkup
2005-09-07 paulson 2005-09-07 elimination of watcher.sig
2005-09-02 quigley 2005-09-02 Added ECommunication.ML
2005-09-02 paulson 2005-09-02 deleted obsolete VampireCommunication.ML
2005-06-28 paulson 2005-06-28 stricter first-order check for meson
2005-06-24 paulson 2005-06-24 meson method taking an argument list
2005-06-20 wenzelm 2005-06-20 use Tools/ATP/VampCommunication.ML;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-26 paulson 2005-05-26 goodby to modUnix
2005-05-23 quigley 2005-05-23 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML. Changed watcher.ML so that the Unix.execute and Unix.reap functions are used instead of those in modUnix.ML, and consequently removed modUnix.ML from Reconstruction.thy
2005-05-19 paulson 2005-05-19 Skolemization of simprules and classical rules
2005-04-28 paulson 2005-04-28 fixed treatment of higher-order simprules
2005-04-19 paulson 2005-04-19 more tidying of libraries in Reconstruction
2005-04-12 paulson 2005-04-12 tweaks mainly to achieve sml/nj compatibility
2005-04-08 paulson 2005-04-08 Reconstruction code, now packaged to avoid name clashes
2005-04-08 paulson 2005-04-08 temporarily removed ATP code
2005-04-07 quigley 2005-04-07 Reconstruction.thy and IsaMakefile updated
2005-04-04 quigley 2005-04-04 Updated to add watcher code.
2005-04-01 paulson 2005-04-01 patch to get it working again
2004-12-07 paulson 2004-12-07 all theories must be related to Reconstruction
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