1.1 --- a/src/HOL/Complex/NSComplex.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Complex/NSComplex.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -412,7 +412,7 @@
     1.4  
     1.5  lemma hcomplex_add_minus_eq_minus:
     1.6        "x + y = (0::hcomplex) ==> x = -y"
     1.7 -apply (drule Ring_and_Field.equals_zero_I)
     1.8 +apply (drule OrderedGroup.equals_zero_I)
     1.9  apply (simp add: minus_equation_iff [of x y])
    1.10  done
    1.11  
    1.12 @@ -429,7 +429,7 @@
    1.13  subsection{*More Multiplication Laws*}
    1.14  
    1.15  lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z"
    1.16 -by (rule Ring_and_Field.mult_1_right)
    1.17 +by (rule OrderedGroup.mult_1_right)
    1.18  
    1.19  lemma hcomplex_mult_minus_one [simp]: "- 1 * (z::hcomplex) = -z"
    1.20  by simp
    1.21 @@ -454,7 +454,7 @@
    1.22  by (simp add: hcomplex_diff_def hcomplex_minus hcomplex_add complex_diff_def)
    1.23  
    1.24  lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
    1.25 -by (rule Ring_and_Field.diff_eq_eq)
    1.26 +by (rule OrderedGroup.diff_eq_eq)
    1.27  
    1.28  lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z"
    1.29  by (rule Ring_and_Field.add_divide_distrib)