| Tue, 30 Jan 1996 13:42:57 +0100 | clasohm | expanded tabs | file | diff | annotate |
| Fri, 28 Apr 1995 11:41:59 +0200 | lcp | Modified proofs for new claset primitives. The problem is that they enforce | file | diff | annotate |
| Thu, 06 Apr 1995 12:06:09 +0200 | lcp | Deleted call to flexflex_tac | file | diff | annotate |
| Fri, 10 Mar 1995 10:20:18 +0100 | lcp | Removed "localize"; instead, proofs refer to their own | file | diff | annotate |
| Wed, 07 Dec 1994 13:12:04 +0100 | clasohm | added qed and qed_goal[w] | file | diff | annotate |
| Fri, 25 Nov 1994 11:04:44 +0100 | lcp | equiv_comp_eq: simplified proof | file | diff | annotate |
| 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 |