replaced translation by abbreviation
authornipkow
Mon Jul 03 20:02:42 2006 +0200 (2006-07-03)
changeset 19979a0846edbe8b0
parent 19978 df19a7876183
child 19980 dc17fd6c0908
replaced translation by abbreviation
src/HOL/Equiv_Relations.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Mon Jul 03 19:33:09 2006 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Jul 03 20:02:42 2006 +0200
     1.3 @@ -221,14 +221,10 @@
     1.4      "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
     1.5  
     1.6  text{*Abbreviation for the common case where the relations are identical*}
     1.7 -syntax
     1.8 -  RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects2 " 80)
     1.9 -translations
    1.10 -  "f respects2 r" => "congruent2 r r f"
    1.11 -(*
    1.12 -Warning: cannot use "abbreviation" here because the two occurrences of
    1.13 -r may need to be of different type (see Hyperreal/StarDef).
    1.14 -*)
    1.15 +abbreviation
    1.16 +  RESPECTS2:: "['a => 'a => 'b, ('a * 'a)set] => bool" (infixr "respects2 " 80)
    1.17 +  "f respects2 r == congruent2 r r f"
    1.18 +
    1.19  
    1.20  lemma congruent2_implies_congruent:
    1.21      "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"