src/HOL/Equiv_Relations.thy
 changeset 19323 ec5cd5b1804c parent 18493 343da052b961 child 19363 667b5ea637dd
```     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Mar 23 18:14:06 2006 +0100
1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Mar 23 20:03:53 2006 +0100
1.3 @@ -163,11 +163,9 @@
1.4    fixes r and f
1.5    assumes congruent: "(y,z) \<in> r ==> f y = f z"
1.6
1.7 -syntax
1.8 -  RESPECTS ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects" 80)
1.9 -
1.10 -translations
1.11 -  "f respects r" == "congruent r f"
1.12 +abbreviation (output)
1.13 +  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  (infixr "respects" 80)
1.14 +  "f respects r = congruent r f"
1.15
1.16
1.17  lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
1.18 @@ -225,9 +223,12 @@
1.19  text{*Abbreviation for the common case where the relations are identical*}
1.20  syntax
1.21    RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects2 " 80)
1.22 -
1.23  translations
1.24    "f respects2 r" => "congruent2 r r f"
1.25 +(*
1.26 +Warning: cannot use "abbreviation" here because the two occurrences of
1.27 +r may need to be of different type (see Hyperreal/StarDef).
1.28 +*)
1.29
1.30  lemma congruent2_implies_congruent:
1.31      "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
1.32 @@ -333,7 +334,7 @@
1.33   apply(fastsimp simp add:inj_on_def)
1.34  apply (simp add:setsum_constant)
1.35  done
1.36 -
1.37 +(*
1.38  ML
1.39  {*
1.40  val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
1.41 @@ -371,5 +372,5 @@
1.42  val subset_equiv_class = thm "subset_equiv_class";
1.43  val sym_trans_comp_subset = thm "sym_trans_comp_subset";
1.44  *}
1.45 -
1.46 +*)
1.47  end
```