src/ZF/EquivClass.thy
 changeset 24892 c663e675e177 parent 23146 0bc590051d95 child 24893 b8ef7afe3a6b
```     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"}*}
```