diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/EquivClass.thy --- a/src/ZF/EquivClass.thy Mon Feb 05 21:33:14 1996 +0100 +++ b/src/ZF/EquivClass.thy Tue Feb 06 12:27:17 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: ZF/EquivClass.thy +(* Title: ZF/EquivClass.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Equivalence relations in Zermelo-Fraenkel Set Theory @@ -9,7 +9,7 @@ EquivClass = Rel + Perm + consts "'/" :: [i,i]=>i (infixl 90) (*set of equiv classes*) - congruent :: [i,i=>i]=>o + congruent :: [i,i=>i]=>o congruent2 :: [i,[i,i]=>i]=>o defs