Wed, 31 May 2000 11:55:51 +0200 | paulson | added new proofs and simplified an old one | changeset | files |
Wed, 31 May 2000 11:55:21 +0200 | paulson | new theorems (some from Multiset) | changeset | files |
Tue, 30 May 2000 18:02:49 +0200 | berghofe | the is now defined using primrec, avoiding explicit use of arbitrary. | changeset | files |