src/HOL/Equiv_Relations.thy
changeset 21749 3f0e86c92ff3
parent 21404 eb85850d3eb7
child 23705 315c638d5856
     1.1 --- a/src/HOL/Equiv_Relations.thy	Sun Dec 10 15:30:48 2006 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Sun Dec 10 15:30:49 2006 +0100
     1.3 @@ -224,7 +224,7 @@
     1.4  text{*Abbreviation for the common case where the relations are identical*}
     1.5  abbreviation
     1.6    RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool"
     1.7 -    (infixr "respects2 " 80) where
     1.8 +    (infixr "respects2" 80) where
     1.9    "f respects2 r == congruent2 r r f"
    1.10  
    1.11