# HG changeset patch
# User wenzelm
# Date 1165761049 -3600
# Node ID 3f0e86c92ff3b144c834b073bba75002f9344222
# Parent  7df0f4e08dde72753e7a4cc42184df26aac72b55
respects2: tuned spacing;

diff -r 7df0f4e08dde -r 3f0e86c92ff3 src/HOL/Equiv_Relations.thy
--- 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"