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