| Wed, 01 May 1996 10:43:16 +0200 | paulson | Provides merge_cs to support default clasets | changeset | files |
| Wed, 01 May 1996 10:38:14 +0200 | paulson | Simplified KG's proofs | changeset | files |
| Wed, 01 May 1996 10:37:07 +0200 | paulson | New lemma inspired by KG | changeset | files |
| Wed, 01 May 1996 10:35:06 +0200 | paulson | tidied some proofs | changeset | files |
| Tue, 30 Apr 1996 17:32:29 +0200 | nipkow | Added an equivalence proof which avoids the use of -n-> | changeset | files |
| Tue, 30 Apr 1996 17:30:54 +0200 | nipkow | Added backwards rtrancl_induct and special versions for pairs. | changeset | files |