src/HOL/Tools/meson.ML
2006-05-26 wenzelm 2006-05-26 freeze_spec: gensym;
2006-03-07 paulson 2006-03-07 Tidying, and getting rid of SELECT_GOAL (as it does something different now)
2006-02-28 paulson 2006-02-28 fixed but in freeze_spec
2006-02-20 paulson 2006-02-20 Fix variable-naming bug (?) by removing a needless recursive call
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-01-28 wenzelm 2006-01-28 LocalDefs.def_export;
2006-01-23 paulson 2006-01-23 Clausification now handles some IFs in rewrite rules (if-split did not work)
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 Output.debug;
2006-01-13 wenzelm 2006-01-13 ProofContext.def_export;
2005-12-23 paulson 2005-12-23 tidied
2005-12-14 paulson 2005-12-14 removal of some redundancies (e.g. one-point-rules) in clause production
2005-12-13 paulson 2005-12-13 removal of functional reflexivity axioms
2005-11-18 mengj 2005-11-18 -- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL. -- added "check_is_fol_term", which is the same as "check_is_fol", but takes a "term" as input. -- added "check_is_fol" and "check_is_fol_term" into the signature.
2005-11-16 paulson 2005-11-16 new version of "tryres" allowing multiple unifiers (apparently needed for Skolemization of higher-order theorems)
2005-11-09 paulson 2005-11-09 Skolemization by inference, but not quite finished
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop;
2005-10-14 paulson 2005-10-14 signature changes
2005-09-29 paulson 2005-09-29 moved concat_with_and to watcher.ML
2005-09-15 paulson 2005-09-15 the experimental tagging system, and the usual tidying
2005-07-13 wenzelm 2005-07-13 tuned concat_with_and; 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-20 paulson 2005-05-20 bug fixes for clause form transformation
2005-05-18 paulson 2005-05-18 new cnf function taking Skolemization theorems as an extra argument
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2005-05-09 paulson 2005-05-09 unfolding of Ex1
2005-05-02 paulson 2005-05-02 meta-logic connectives now forbidden
2005-04-28 paulson 2005-04-28 fixed treatment of higher-order simprules
2005-04-27 paulson 2005-04-27 removed unnecessary (?) check
2005-04-20 quigley 2005-04-20 Removed remaining references to Main.thy in reconstruction code.
2005-04-19 quigley 2005-04-19 Completed integration of reconstruction code. Now finds and displays proofs when used with modified version of Proof General. C.Q.
2005-04-15 paulson 2005-04-15 more tidying up of the SPASS interface
2005-04-12 paulson 2005-04-12 tweaks mainly to achieve sml/nj compatibility
2005-04-07 quigley 2005-04-07 Integrating the reconstruction files into the building of HOL
2005-04-04 quigley 2005-04-04 Updated to add watcher code.
2005-03-17 paulson 2005-03-17 meson now checks that problems are first-order
2005-03-07 paulson 2005-03-07 now checks for higher-order vars
2005-03-07 paulson 2005-03-07 Tools/meson.ML: signature, structure and "open" rather than "local"
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-21 paulson 2005-01-21 negate_nead (???) changed to negated_asm_of_head
2004-08-20 paulson 2004-08-20 proof reconstruction for external ATPs
2004-08-06 paulson 2004-08-06 make_clauses now meta
2004-07-11 wenzelm 2004-07-11 local_cla/simpset_of;
2004-06-28 paulson 2004-06-28 new method for explicit classical resolution
2004-06-09 paulson 2004-06-09 fixed the skolemize method
2004-05-28 paulson 2004-05-28 new skolemize_tac and skolemize method
2004-05-19 paulson 2004-05-19 has_consts now handles the @-operator
2004-05-14 paulson 2004-05-14 clauses for ordinary resolution
2004-05-11 paulson 2004-05-11 conversion to clauses for ordinary resolution rather than ME
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2001-11-26 wenzelm 2001-11-26 moved lemmas to theory Hilbert_Choice;
2001-01-07 wenzelm 2001-01-07 CHANGED_PROP;
2000-09-05 wenzelm 2000-09-05 improved meson setup;
2000-09-05 paulson 2000-09-05 meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default