src/HOL/Tools/res_axioms.ML
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago Output.debug;
2006-01-10 ago Attrib.rule;
2005-12-31 ago elim rules: Classical.classical_rule;
2005-12-23 ago the "skolem" attribute and better initialization of the clause database
2005-12-14 ago removed unused function repeat_RS
2005-11-28 ago Added two functions for CNF translation, used by other files.
2005-11-18 ago -- 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 ago duplicate axioms in ATP linkup, and general fixes
2005-11-09 ago Skolemization by inference, but not quite finished
2005-10-28 ago got rid of obsolete prove_goalw_cterm
2005-10-28 ago 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.
2005-10-21 ago OldGoals;
2005-10-19 ago 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 ago simplifying the treatment of clausification
2005-10-10 ago small tidy-up of utility functions
2005-09-19 ago simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-15 ago the experimental tagging system, and the usual tidying
2005-09-06 ago tuned comments;
2005-09-05 ago curried_lookup/update;
2005-07-27 ago simpler variable names, and no types for monomorphic constants
2005-07-20 ago code streamlining
2005-07-13 ago improved Net interface;
2005-06-28 ago stricter first-order check for meson
2005-06-24 ago meson method taking an argument list
2005-06-01 ago clausification bug fix
2005-05-31 ago Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
2005-05-31 ago proper use of Sign.full_name;
2005-05-23 ago Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
2005-05-20 ago bug fixes for clause form transformation
2005-05-19 ago Skolemization of simprules and classical rules
2005-05-18 ago consolidation and simplification
2005-05-12 ago theorem names for caching
2005-05-12 ago memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
2005-04-28 ago fixed treatment of higher-order simprules
2005-04-15 ago more tidying up of the SPASS interface
2005-04-08 ago Reconstruction code, now packaged to avoid name clashes
2005-03-31 ago *** empty log message ***
2005-03-14 ago bug fixes involving typechecking clauses
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
2004-12-09 ago Comments and other tweaks by Jia
2004-12-03 ago fixes to clause conversion
2004-12-03 ago trying to fix the transfer problem
2004-12-02 ago new CLAUSIFY attribute for proof reconstruction with lemmas
2004-11-30 ago resolution package tools by Jia Meng