src/ZF/EquivClass.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/EquivClass.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/EquivClass.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,9 +8,9 @@
     1.4  
     1.5  EquivClass = Rel + Perm + 
     1.6  consts
     1.7 -    "'/"        ::      "[i,i]=>i"  (infixl 90)  (*set of equiv classes*)
     1.8 -    congruent	::	"[i,i=>i]=>o"
     1.9 -    congruent2  ::      "[i,[i,i]=>i]=>o"
    1.10 +    "'/"        ::      [i,i]=>i  (infixl 90)  (*set of equiv classes*)
    1.11 +    congruent	::	[i,i=>i]=>o
    1.12 +    congruent2  ::      [i,[i,i]=>i]=>o
    1.13  
    1.14  defs
    1.15      quotient_def  "A/r == {r``{x} . x:A}"