1.1 --- a/src/ZF/EquivClass.thy	Sun Oct 07 13:57:05 2007 +0200
     1.2 +++ b/src/ZF/EquivClass.thy	Sun Oct 07 15:49:25 2007 +0200
     1.3 @@ -21,14 +21,15 @@
     1.4        "congruent2(r1,r2,b) == ALL y1 z1 y2 z2.
     1.5             <y1,z1>:r1 --> <y2,z2>:r2 --> b(y1,y2) = b(z1,z2)"
     1.6  
     1.7 -syntax
     1.8 -  RESPECTS ::"[i=>i, i] => o"  (infixr "respects" 80)
     1.9 -  RESPECTS2 ::"[i=>i, i] => o"  (infixr "respects2 " 80)
    1.10 +abbreviation
    1.11 +  RESPECTS ::"[i=>i, i] => o"  (infixr "respects" 80) where
    1.12 +  "f respects r == congruent(r,f)"
    1.13 +
    1.14 +abbreviation
    1.15 +  RESPECTS2 ::"[i=>i=>i, i] => o"  (infixr "respects2 " 80) where
    1.16 +  "f respects2 r == congruent2(r,r,f)"
    1.17      --{*Abbreviation for the common case where the relations are identical*}
    1.18  
    1.19 -translations
    1.20 -  "f respects r" == "congruent(r,f)"
    1.21 -  "f respects2 r" => "congruent2(r,r,f)"
    1.22  
    1.23  subsection{*Suppes, Theorem 70:
    1.24      @{term r} is an equiv relation iff @{term "converse(r) O r = r"}*}