src/HOL/Tools/meson.ML
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