src/HOL/Equiv_Relations.thy
changeset 21404 eb85850d3eb7
parent 19979 a0846edbe8b0
child 21749 3f0e86c92ff3
     1.1 --- a/src/HOL/Equiv_Relations.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -164,7 +164,8 @@
     1.4    assumes congruent: "(y,z) \<in> r ==> f y = f z"
     1.5  
     1.6  abbreviation
     1.7 -  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  (infixr "respects" 80)
     1.8 +  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"
     1.9 +    (infixr "respects" 80) where
    1.10    "f respects r == congruent r f"
    1.11  
    1.12  
    1.13 @@ -222,7 +223,8 @@
    1.14  
    1.15  text{*Abbreviation for the common case where the relations are identical*}
    1.16  abbreviation
    1.17 -  RESPECTS2:: "['a => 'a => 'b, ('a * 'a)set] => bool" (infixr "respects2 " 80)
    1.18 +  RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool"
    1.19 +    (infixr "respects2 " 80) where
    1.20    "f respects2 r == congruent2 r r f"
    1.21  
    1.22