diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue May 11 14:00:02 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Tue May 11 20:11:08 2004 +0200
@@ -169,7 +169,7 @@
 lemma real_add_zero_left: "(0::real) + z = z"
 by (cases z, simp add: real_add real_zero_def preal_add_ac)
 
-instance real :: plus_ac0
+instance real :: comm_monoid_add
   by (intro_classes,
       (assumption | 
        rule real_add_commute real_add_assoc real_add_zero_left)+)
@@ -281,9 +281,6 @@
 instance real :: field
 proof
   fix x y z :: real
-  show "(x + y) + z = x + (y + z)" by (rule real_add_assoc)
-  show "x + y = y + x" by (rule real_add_commute)
-  show "0 + x = x" by simp
   show "- x + x = 0" by (rule real_add_minus_left)
   show "x - y = x + (-y)" by (simp add: real_diff_def)
   show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
@@ -312,7 +309,7 @@
         minus_mult_left [symmetric, simp]
 
 lemma real_mult_1_right: "z * (1::real) = z"
-  by (rule Ring_and_Field.mult_1_right)
+  by (rule OrderedGroup.mult_1_right)
 
 
 subsection{*The @{text "\<le>"} Ordering*}
@@ -554,11 +551,11 @@
 by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
 
 lemma real_add_less_le_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::real)"
-  by (rule Ring_and_Field.add_less_le_mono)
+  by (rule OrderedGroup.add_less_le_mono)
 
 lemma real_add_le_less_mono:
      "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
-  by (rule Ring_and_Field.add_le_less_mono)
+  by (rule OrderedGroup.add_le_less_mono)
 
 lemma real_le_square [simp]: "(0::real) \<le> x*x"
  by (rule Ring_and_Field.zero_le_square)
@@ -597,7 +594,7 @@
 
 text{*FIXME: delete or at least combine the next two lemmas*}
 lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
-apply (drule Ring_and_Field.equals_zero_I [THEN sym])
+apply (drule OrderedGroup.equals_zero_I [THEN sym])
 apply (cut_tac x = y in real_le_square) 
 apply (auto, drule order_antisym, auto)
 done
@@ -848,7 +845,7 @@
 by (force simp add: Ring_and_Field.abs_less_iff)
 
 lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
-by (force simp add: Ring_and_Field.abs_le_iff)
+by (force simp add: OrderedGroup.abs_le_iff)
 
 (*FIXME: used only once, in SEQ.ML*)
 lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
@@ -892,7 +889,7 @@
 val abs_minus_eqI2 = thm"abs_minus_eqI2";
 val abs_ge_zero = thm"abs_ge_zero";
 val abs_idempotent = thm"abs_idempotent";
-val abs_zero_iff = thm"abs_zero_iff";
+val abs_eq_0 = thm"abs_eq_0";
 val abs_ge_self = thm"abs_ge_self";
 val abs_ge_minus_self = thm"abs_ge_minus_self";
 val abs_mult = thm"abs_mult";