2006-04-18 mengj 2006-04-18 Tidied up some programs.
2006-04-07 mengj 2006-04-07 added another function for CNF.
2006-03-10 paulson 2006-03-10 Changed some warnings to debug messages
2006-03-07 paulson 2006-03-07 Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before. Removal of the unused err_list.
2006-03-07 mengj 2006-03-07 Added functions to retrieve local and global atpset rules. cnf thms to Term.term format.
2006-03-02 paulson 2006-03-02 subset_refl now included using the atp attribute
2006-02-20 paulson 2006-02-20 Inclusion of subset_refl in ATP calls
2006-02-03 paulson 2006-02-03 removal of case analysis clauses
2006-01-29 wenzelm 2006-01-29 tuned comment;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 Output.debug;
2006-01-10 wenzelm 2006-01-10 Attrib.rule;
2005-12-31 wenzelm 2005-12-31 elim rules: Classical.classical_rule;
2005-12-23 paulson 2005-12-23 the "skolem" attribute and better initialization of the clause database
2005-12-14 paulson 2005-12-14 removed unused function repeat_RS
2005-11-28 mengj 2005-11-28 Added two functions for CNF translation, used by other files.
2005-11-18 mengj 2005-11-18 -- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
2005-11-10 paulson 2005-11-10 duplicate axioms in ATP linkup, and general fixes
2005-11-09 paulson 2005-11-09 Skolemization by inference, but not quite finished
2005-10-28 paulson 2005-10-28 got rid of obsolete prove_goalw_cterm
2005-10-28 mengj 2005-10-28 Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names. Also added function "repeat_RS" to the signature.
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-19 mengj 2005-10-19 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
2005-10-11 paulson 2005-10-11 simplifying the treatment of clausification
2005-10-10 paulson 2005-10-10 small tidy-up of utility functions
2005-09-19 paulson 2005-09-19 simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-15 paulson 2005-09-15 the experimental tagging system, and the usual tidying
2005-09-06 wenzelm 2005-09-06 tuned comments;
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-07-27 paulson 2005-07-27 simpler variable names, and no types for monomorphic constants
2005-07-20 paulson 2005-07-20 code streamlining
2005-07-13 wenzelm 2005-07-13 improved Net interface;
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-01 paulson 2005-06-01 clausification bug fix
2005-05-31 quigley 2005-05-31 Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass ruleset.
2005-05-31 wenzelm 2005-05-31 proper use of Sign.full_name;
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-20 paulson 2005-05-20 bug fixes for clause form transformation
2005-05-19 paulson 2005-05-19 Skolemization of simprules and classical rules
2005-05-18 paulson 2005-05-18 consolidation and simplification
2005-05-12 paulson 2005-05-12 theorem names for caching
2005-05-12 paulson 2005-05-12 memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
2005-04-28 paulson 2005-04-28 fixed treatment of higher-order simprules
2005-04-15 paulson 2005-04-15 more tidying up of the SPASS interface
2005-04-08 paulson 2005-04-08 Reconstruction code, now packaged to avoid name clashes
2005-03-31 quigley 2005-03-31 *** empty log message ***
2005-03-14 paulson 2005-03-14 bug fixes involving typechecking clauses
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
2004-12-09 paulson 2004-12-09 Comments and other tweaks by Jia
2004-12-03 paulson 2004-12-03 fixes to clause conversion
2004-12-03 paulson 2004-12-03 trying to fix the transfer problem
2004-12-02 paulson 2004-12-02 new CLAUSIFY attribute for proof reconstruction with lemmas
2004-11-30 paulson 2004-11-30 resolution package tools by Jia Meng