# HG changeset patch
# User nipkow
# Date 1151949762 -7200
# Node ID a0846edbe8b0b119eaf44ef567fff6611ed4bebf
# Parent  df19a78761831e3519119f2843de7e52fe6463ff
replaced translation by abbreviation

diff -r df19a7876183 -r a0846edbe8b0 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Mon Jul 03 19:33:09 2006 +0200
+++ b/src/HOL/Equiv_Relations.thy	Mon Jul 03 20:02:42 2006 +0200
@@ -221,14 +221,10 @@
     "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
 
 text{*Abbreviation for the common case where the relations are identical*}
-syntax
-  RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects2 " 80)
-translations
-  "f respects2 r" => "congruent2 r r f"
-(*
-Warning: cannot use "abbreviation" here because the two occurrences of
-r may need to be of different type (see Hyperreal/StarDef).
-*)
+abbreviation
+  RESPECTS2:: "['a => 'a => 'b, ('a * 'a)set] => bool" (infixr "respects2 " 80)
+  "f respects2 r == congruent2 r r f"
+
 
 lemma congruent2_implies_congruent:
     "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"