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