src/HOL/Equiv_Relations.thy

--- a/src/HOL/Equiv_Relations.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Equiv_Relations.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -163,9 +163,9 @@
   fixes r and f
   assumes congruent: "(y,z) \<in> r ==> f y = f z"
 
-abbreviation (output)
+abbreviation
   RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  (infixr "respects" 80)
-  "f respects r = congruent r f"
+  "f respects r == congruent r f"
 
 
 lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"