src/HOL/Algebra/abstract/Ring2.thy
changeset 25762 c03e9d04b3e4
parent 24993 92dfacb32053
child 26342 0f65fa163304
     1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Jan 02 12:22:38 2008 +0100
     1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Jan 02 15:14:02 2008 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5  subsection {* Ring axioms *}
     1.6  
     1.7 -axclass ring < zero, one, plus, minus, times, inverse, power, Divides.div
     1.8 +axclass ring < zero, one, plus, minus, uminus, times, inverse, power, Divides.div
     1.9  
    1.10    a_assoc:      "(a + b) + c = a + (b + c)"
    1.11    l_zero:       "0 + a = a"