1.1 --- a/src/HOL/Real/RealDef.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -169,7 +169,7 @@
     1.4  lemma real_add_zero_left: "(0::real) + z = z"
     1.5  by (cases z, simp add: real_add real_zero_def preal_add_ac)
     1.6  
     1.7 -instance real :: plus_ac0
     1.8 +instance real :: comm_monoid_add
     1.9    by (intro_classes,
    1.10        (assumption | 
    1.11         rule real_add_commute real_add_assoc real_add_zero_left)+)
    1.12 @@ -281,9 +281,6 @@
    1.13  instance real :: field
    1.14  proof
    1.15    fix x y z :: real
    1.16 -  show "(x + y) + z = x + (y + z)" by (rule real_add_assoc)
    1.17 -  show "x + y = y + x" by (rule real_add_commute)
    1.18 -  show "0 + x = x" by simp
    1.19    show "- x + x = 0" by (rule real_add_minus_left)
    1.20    show "x - y = x + (-y)" by (simp add: real_diff_def)
    1.21    show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
    1.22 @@ -312,7 +309,7 @@
    1.23          minus_mult_left [symmetric, simp]
    1.24  
    1.25  lemma real_mult_1_right: "z * (1::real) = z"
    1.26 -  by (rule Ring_and_Field.mult_1_right)
    1.27 +  by (rule OrderedGroup.mult_1_right)
    1.28  
    1.29  
    1.30  subsection{*The @{text "\<le>"} Ordering*}
    1.31 @@ -554,11 +551,11 @@
    1.32  by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
    1.33  
    1.34  lemma real_add_less_le_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::real)"
    1.35 -  by (rule Ring_and_Field.add_less_le_mono)
    1.36 +  by (rule OrderedGroup.add_less_le_mono)
    1.37  
    1.38  lemma real_add_le_less_mono:
    1.39       "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
    1.40 -  by (rule Ring_and_Field.add_le_less_mono)
    1.41 +  by (rule OrderedGroup.add_le_less_mono)
    1.42  
    1.43  lemma real_le_square [simp]: "(0::real) \<le> x*x"
    1.44   by (rule Ring_and_Field.zero_le_square)
    1.45 @@ -597,7 +594,7 @@
    1.46  
    1.47  text{*FIXME: delete or at least combine the next two lemmas*}
    1.48  lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
    1.49 -apply (drule Ring_and_Field.equals_zero_I [THEN sym])
    1.50 +apply (drule OrderedGroup.equals_zero_I [THEN sym])
    1.51  apply (cut_tac x = y in real_le_square) 
    1.52  apply (auto, drule order_antisym, auto)
    1.53  done
    1.54 @@ -848,7 +845,7 @@
    1.55  by (force simp add: Ring_and_Field.abs_less_iff)
    1.56  
    1.57  lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
    1.58 -by (force simp add: Ring_and_Field.abs_le_iff)
    1.59 +by (force simp add: OrderedGroup.abs_le_iff)
    1.60  
    1.61  (*FIXME: used only once, in SEQ.ML*)
    1.62  lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
    1.63 @@ -892,7 +889,7 @@
    1.64  val abs_minus_eqI2 = thm"abs_minus_eqI2";
    1.65  val abs_ge_zero = thm"abs_ge_zero";
    1.66  val abs_idempotent = thm"abs_idempotent";
    1.67 -val abs_zero_iff = thm"abs_zero_iff";
    1.68 +val abs_eq_0 = thm"abs_eq_0";
    1.69  val abs_ge_self = thm"abs_ge_self";
    1.70  val abs_ge_minus_self = thm"abs_ge_minus_self";
    1.71  val abs_mult = thm"abs_mult";