2006-10-20 ago nclauses no longer requires its input to be in NNF
2006-10-18 ago More robust error handling in make_nnf and forward_res
2006-10-16 ago moved HOL code generator setup to Code_Generator
2006-10-11 ago abandoned findrep
2006-10-02 ago Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.
2006-09-13 ago Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective
2006-08-25 ago better skolemization, using first-order resolution rather than hoping for the right result
2006-08-08 ago more explict variable names
2006-08-02 ago simplified Assumption/ProofContext.export;
2006-07-16 ago has_consts renamed to has_conn, now actually parses the first-order formula
2006-07-13 ago fix to refl_clause_aux: added occurs check
2006-07-11 ago removed obsolete mem_term;
2006-07-05 ago removed the "tagging" feature
2006-06-15 ago the "all_theorems" option and some fixes
2006-06-13 ago avoid unqualified exception names;
2006-05-26 ago freeze_spec: gensym;
2006-03-07 ago Tidying, and getting rid of SELECT_GOAL (as it does something different now)
2006-02-28 ago fixed but in freeze_spec
2006-02-20 ago Fix variable-naming bug (?) by removing a needless recursive call
2006-02-15 ago removed distinct, renamed gen_distinct to distinct;
2006-01-28 ago LocalDefs.def_export;
2006-01-23 ago Clausification now handles some IFs in rewrite rules (if-split did not work)
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago Output.debug;
2006-01-13 ago ProofContext.def_export;
2005-12-23 ago tidied
2005-12-14 ago removal of some redundancies (e.g. one-point-rules) in clause production
2005-12-13 ago removal of functional reflexivity axioms
2005-11-18 ago -- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
2005-11-16 ago new version of "tryres" allowing multiple unifiers (apparently needed for
2005-11-09 ago Skolemization by inference, but not quite finished
2005-10-28 ago renamed Goal constant to prop;
2005-10-14 ago signature changes
2005-09-29 ago moved concat_with_and to watcher.ML
2005-09-15 ago the experimental tagging system, and the usual tidying
2005-07-13 ago tuned concat_with_and;
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-20 ago bug fixes for clause form transformation
2005-05-18 ago new cnf function taking Skolemization theorems as an extra argument
2005-05-16 ago Use of instead of int in most numeric simprocs; avoids
2005-05-09 ago unfolding of Ex1
2005-05-02 ago meta-logic connectives now forbidden
2005-04-28 ago fixed treatment of higher-order simprules
2005-04-27 ago removed unnecessary (?) check
2005-04-20 ago Removed remaining references to Main.thy in reconstruction code.
2005-04-19 ago Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
2005-04-15 ago more tidying up of the SPASS interface
2005-04-12 ago tweaks mainly to achieve sml/nj compatibility
2005-04-07 ago Integrating the reconstruction files into the building of HOL
2005-04-04 ago Updated to add watcher code.
2005-03-17 ago meson now checks that problems are first-order
2005-03-07 ago now checks for higher-order vars
2005-03-07 ago Tools/meson.ML: signature, structure and "open" rather than "local"
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-21 ago negate_nead (???) changed to negated_asm_of_head
2004-08-20 ago proof reconstruction for external ATPs