src/FOL/IFOL.ML
Wed, 25 Aug 1999 20:45:19 +0200 wenzelm proper bootstrap of IFOL/FOL theories and packages;
Sat, 10 Jul 1999 21:44:26 +0200 wenzelm handle THM exn;
Wed, 13 Jan 1999 12:08:18 +0100 paulson generalized qed_spec_mp code to work for ZF
Tue, 12 Jan 1999 13:39:41 +0100 wenzelm eliminated Attribute structure;
Tue, 01 Dec 1998 14:48:24 +0100 wenzelm removed duplicate contrapos;
Mon, 16 Nov 1998 11:11:58 +0100 wenzelm attrib_setup: rulify;
Thu, 13 Aug 1998 17:28:52 +0200 paulson stac now handles definitions as well as equalities
Tue, 14 Jul 1998 13:29:39 +0200 paulson stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
Mon, 22 Dec 1997 11:16:47 +0100 paulson New rules rev_iffD{1,2}
Fri, 07 Nov 1997 17:51:26 +0100 oheimb added contrapos
Fri, 10 Oct 1997 15:52:12 +0200 wenzelm fixed dots;
Mon, 29 Sep 1997 11:32:25 +0200 paulson qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
Thu, 27 Mar 1997 10:06:36 +0100 paulson Updated comment
Thu, 26 Sep 1996 17:02:51 +0200 paulson Declared stac
Fri, 26 Jul 1996 12:31:04 +0200 paulson Addition of rev_notE
Tue, 26 Mar 1996 11:38:17 +0100 paulson Added two of KGs rules
Mon, 29 Jan 1996 13:58:15 +0100 clasohm expanded tabs
Fri, 13 Oct 1995 11:48:40 +0100 clasohm corrected spelling of title
Thu, 06 Apr 1995 10:58:56 +0200 lcp Fixed typo.
Fri, 23 Dec 1994 10:52:25 +0100 lcp Added Krzysztof's theorem disj_imp_disj
Fri, 16 Dec 1994 13:30:34 +0100 lcp conj_cong2: new congruence rule
Tue, 13 Dec 1994 11:51:12 +0100 clasohm removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
Fri, 24 Sep 1993 11:13:55 +0200 lcp Added ex_ex1I: new introduction rule for the EX! quantifier.
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip