src/HOL/Equiv_Relations.thy

 text{*A congruence-preserving function*}
 locale congruent =
   fixes r and f
   assumes congruent: "(y,z) \<in> r ==> f y = f z"
 
-syntax
-  RESPECTS ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects" 80)
-
-translations
-  "f respects r" == "congruent r f"
+abbreviation (output)
+  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  (infixr "respects" 80)
+  "f respects r = congruent r f"
 
 
 lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
   -- {* lemma required to prove @{text UN_equiv_class} *}
   by auto

     "(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).
+*)
 
 lemma congruent2_implies_congruent:
     "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
   by (unfold congruent_def congruent2_def equiv_def refl_def) blast
 

    apply assumption
   apply simp
  apply(fastsimp simp add:inj_on_def)
 apply (simp add:setsum_constant)
 done
-
+(*
 ML
 {*
 val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
 val UN_constant_eq = thm "UN_constant_eq";
 val UN_equiv_class = thm "UN_equiv_class";

 val quotient_disj = thm "quotient_disj";
 val refl_comp_subset = thm "refl_comp_subset";
 val subset_equiv_class = thm "subset_equiv_class";
 val sym_trans_comp_subset = thm "sym_trans_comp_subset";
 *}
-
+*)
 end