| Wed, 14 Dec 1994 16:57:55 +0100 |
lcp |
converse_UN, Diff_eq_0_iff: new
|
file |
diff |
annotate
|
| Wed, 07 Dec 1994 13:12:04 +0100 |
clasohm |
added qed and qed_goal[w]
|
file |
diff |
annotate
|
| Thu, 03 Nov 1994 11:58:16 +0100 |
lcp |
ZF/equalities/domain_converse,range_converse,
|
file |
diff |
annotate
|
| Tue, 16 Aug 1994 19:09:43 +0200 |
lcp |
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
|
file |
diff |
annotate
|
| Mon, 15 Aug 1994 18:07:03 +0200 |
lcp |
ZF/equalities/Sigma_cons: new
|
file |
diff |
annotate
|
| Fri, 12 Aug 1994 18:45:33 +0200 |
lcp |
for infinite datatypes with arbitrary index sets
|
file |
diff |
annotate
|
| Tue, 21 Jun 1994 17:20:34 +0200 |
lcp |
Addition of cardinals and order types, various tidying
|
file |
diff |
annotate
|
| Mon, 14 Feb 1994 17:59:25 +0100 |
lcp |
double_complement_Un: new
|
file |
diff |
annotate
|
| Tue, 21 Dec 1993 13:58:12 +0100 |
lcp |
new section for equality properties
|
file |
diff |
annotate
|
| Fri, 10 Dec 1993 10:39:12 +0100 |
lcp |
ZF/equalities/SUM_eq_UN: new
|
file |
diff |
annotate
|
| Fri, 03 Dec 1993 12:47:45 +0100 |
lcp |
New distributive laws for Sigma and UN
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|