src/HOL/Equiv_Relations.thy
changeset 19363 667b5ea637dd
parent 19323 ec5cd5b1804c
child 19979 a0846edbe8b0
     1.1 --- a/src/HOL/Equiv_Relations.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -163,9 +163,9 @@
     1.4    fixes r and f
     1.5    assumes congruent: "(y,z) \<in> r ==> f y = f z"
     1.6  
     1.7 -abbreviation (output)
     1.8 +abbreviation
     1.9    RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  (infixr "respects" 80)
    1.10 -  "f respects r = congruent r f"
    1.11 +  "f respects r == congruent r f"
    1.12  
    1.13  
    1.14  lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"