src/HOL/Hyperreal/HyperDef.thy
changeset 14738 83f1a514dcb4
parent 14705 14b2c22a7e40
child 15013 34264f5e4691
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -332,7 +332,7 @@
     1.4  lemma hypreal_add_zero_left: "(0::hypreal) + z = z"
     1.5  by (cases z, simp add: hypreal_zero_def hypreal_add)
     1.6  
     1.7 -instance hypreal :: plus_ac0
     1.8 +instance hypreal :: comm_monoid_add
     1.9    by intro_classes
    1.10      (assumption | 
    1.11        rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+
    1.12 @@ -423,9 +423,6 @@
    1.13  instance hypreal :: field
    1.14  proof
    1.15    fix x y z :: hypreal
    1.16 -  show "(x + y) + z = x + (y + z)" by (rule hypreal_add_assoc)
    1.17 -  show "x + y = y + x" by (rule hypreal_add_commute)
    1.18 -  show "0 + x = x" by simp
    1.19    show "- x + x = 0" by (simp add: hypreal_add_minus_left)
    1.20    show "x - y = x + (-y)" by (simp add: hypreal_diff_def)
    1.21    show "(x * y) * z = x * (y * z)" by (rule hypreal_mult_assoc)
    1.22 @@ -512,7 +509,7 @@
    1.23  
    1.24  lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
    1.25  apply auto
    1.26 -apply (rule Ring_and_Field.add_right_cancel [of _ "-y", THEN iffD1], auto)
    1.27 +apply (rule OrderedGroup.add_right_cancel [of _ "-y", THEN iffD1], auto)
    1.28  done
    1.29  
    1.30  lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"