| Mon, 21 Nov 1994 13:47:00 +0100 | lcp | ZF/EquivClass/congruent_commuteI: uncommented and simplified proof | file | diff | annotate |
| Tue, 16 Aug 1994 19:06:14 +0200 | lcp | ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML | file | diff | annotate |