--- a/src/HOL/Equiv_Relations.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Equiv_Relations.thy Fri Nov 17 02:20:03 2006 +0100
@@ -164,7 +164,8 @@
assumes congruent: "(y,z) \<in> r ==> f y = f z"
abbreviation
- RESPECTS :: "('a => 'b) => ('a * 'a) set => bool" (infixr "respects" 80)
+ RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"
+ (infixr "respects" 80) where
"f respects r == congruent r f"
@@ -222,7 +223,8 @@
text{*Abbreviation for the common case where the relations are identical*}
abbreviation
- RESPECTS2:: "['a => 'a => 'b, ('a * 'a)set] => bool" (infixr "respects2 " 80)
+ RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool"
+ (infixr "respects2 " 80) where
"f respects2 r == congruent2 r r f"