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
2004-08-06 ago make_clauses now meta
2004-07-11 ago local_cla/simpset_of;
2004-06-28 ago new method for explicit classical resolution
2004-06-09 ago fixed the skolemize method
2004-05-28 ago new skolemize_tac and skolemize method
2004-05-19 ago has_consts now handles the @-operator
2004-05-14 ago clauses for ordinary resolution
2004-05-11 ago conversion to clauses for ordinary resolution rather than ME
2002-05-07 ago use eq_thm_prop instead of slightly inadequate eq_thm;
2001-11-26 ago moved lemmas to theory Hilbert_Choice;
2001-01-07 ago CHANGED_PROP;
2000-09-05 ago improved meson setup;
2000-09-05 ago meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default