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
|