author | wenzelm |
Sun, 10 Dec 2006 15:30:49 +0100 | |
changeset 21749 | 3f0e86c92ff3 |
parent 21748 | 7df0f4e08dde |
child 21750 | 41986849fee0 |
--- a/src/HOL/Equiv_Relations.thy Sun Dec 10 15:30:48 2006 +0100 +++ b/src/HOL/Equiv_Relations.thy Sun Dec 10 15:30:49 2006 +0100 @@ -224,7 +224,7 @@ text{*Abbreviation for the common case where the relations are identical*} abbreviation RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool" - (infixr "respects2 " 80) where + (infixr "respects2" 80) where "f respects2 r == congruent2 r r f"