src/HOL/Algebra/abstract/Ring2.thy
changeset 31001 7e6ffd8f51a9
parent 30968 10fef94f40fc
child 32010 cb1a1c94b4cd
     1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Mon Apr 27 08:22:37 2009 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Mon Apr 27 10:11:44 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 + recpower + Ring_and_Field.dvd +
     1.8 +class ring = zero + one + plus + minus + uminus + times + inverse + power + 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"