src/HOL/Tools/meson.ML
Mon, 02 May 2005 16:28:33 +0200 paulson meta-logic connectives now forbidden
Thu, 28 Apr 2005 17:56:58 +0200 paulson fixed treatment of higher-order simprules
Wed, 27 Apr 2005 16:40:27 +0200 paulson removed unnecessary (?) check
Wed, 20 Apr 2005 16:03:17 +0200 quigley Removed remaining references to Main.thy in reconstruction code.
Tue, 19 Apr 2005 15:15:06 +0200 quigley Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
Fri, 15 Apr 2005 13:35:53 +0200 paulson more tidying up of the SPASS interface
Tue, 12 Apr 2005 11:08:25 +0200 paulson tweaks mainly to achieve sml/nj compatibility
Thu, 07 Apr 2005 18:20:04 +0200 quigley Integrating the reconstruction files into the building of HOL
Mon, 04 Apr 2005 18:43:18 +0200 quigley Updated to add watcher code.
Thu, 17 Mar 2005 15:12:03 +0100 paulson meson now checks that problems are first-order
Mon, 07 Mar 2005 18:40:36 +0100 paulson now checks for higher-order vars
Mon, 07 Mar 2005 16:55:36 +0100 paulson Tools/meson.ML: signature, structure and "open" rather than "local"
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Fri, 21 Jan 2005 13:52:57 +0100 paulson negate_nead (???) changed to negated_asm_of_head
Fri, 20 Aug 2004 12:21:03 +0200 paulson proof reconstruction for external ATPs
Fri, 06 Aug 2004 13:36:04 +0200 paulson make_clauses now meta
Sun, 11 Jul 2004 20:33:22 +0200 wenzelm local_cla/simpset_of;
Mon, 28 Jun 2004 11:15:13 +0200 paulson new method for explicit classical resolution
Wed, 09 Jun 2004 11:19:23 +0200 paulson fixed the skolemize method
Fri, 28 May 2004 11:20:04 +0200 paulson new skolemize_tac and skolemize method
Wed, 19 May 2004 11:31:26 +0200 paulson has_consts now handles the @-operator
Fri, 14 May 2004 16:49:12 +0200 paulson clauses for ordinary resolution
Tue, 11 May 2004 10:48:00 +0200 paulson conversion to clauses for ordinary resolution rather than ME
Tue, 07 May 2002 14:26:32 +0200 wenzelm use eq_thm_prop instead of slightly inadequate eq_thm;
Mon, 26 Nov 2001 18:34:17 +0100 wenzelm moved lemmas to theory Hilbert_Choice;
Sun, 07 Jan 2001 21:41:56 +0100 wenzelm CHANGED_PROP;
Tue, 05 Sep 2000 21:06:01 +0200 wenzelm improved meson setup;
Tue, 05 Sep 2000 10:15:23 +0200 paulson meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
less more (0) tip