1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Thu Apr 23 12:17:51 2009 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Thu Apr 23 12:17:51 2009 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  subsection {* Ring axioms *}
     1.6  
     1.7 -class ring = zero + one + plus + minus + uminus + times + inverse + power + Ring_and_Field.dvd +
     1.8 +class ring = zero + one + plus + minus + uminus + times + inverse + recpower + Ring_and_Field.dvd +
     1.9    assumes a_assoc:      "(a + b) + c = a + (b + c)"
    1.10    and l_zero:           "0 + a = a"
    1.11    and l_neg:            "(-a) + a = 0"
    1.12 @@ -28,8 +28,6 @@
    1.13    assumes minus_def:    "a - b = a + (-b)"
    1.14    and inverse_def:      "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
    1.15    and divide_def:       "a / b = a * inverse b"
    1.16 -  and power_0 [simp]:   "a ^ 0 = 1"
    1.17 -  and power_Suc [simp]: "a ^ Suc n = a ^ n * a"
    1.18  begin
    1.19  
    1.20  definition assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50) where