src/HOL/Algebra/abstract/Ring2.thy
changeset 24993 92dfacb32053
parent 23894 1a4167d761ac
child 25762 c03e9d04b3e4
     1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Fri Oct 12 08:20:45 2007 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Fri Oct 12 08:20:46 2007 +0200
     1.3 @@ -15,15 +15,15 @@
     1.4  text {* Most constants are already declared by HOL. *}
     1.5  
     1.6  consts
     1.7 -  assoc         :: "['a::times, 'a] => bool"              (infixl "assoc" 50)
     1.8 -  irred         :: "'a::{zero, one, times} => bool"
     1.9 -  prime         :: "'a::{zero, one, times} => bool"
    1.10 +  assoc         :: "['a::Divides.div, 'a] => bool"              (infixl "assoc" 50)
    1.11 +  irred         :: "'a::{zero, one, Divides.div} => bool"
    1.12 +  prime         :: "'a::{zero, one, Divides.div} => bool"
    1.13  
    1.14  section {* Axioms *}
    1.15  
    1.16  subsection {* Ring axioms *}
    1.17  
    1.18 -axclass ring < zero, one, plus, minus, times, inverse, power
    1.19 +axclass ring < zero, one, plus, minus, times, inverse, power, Divides.div
    1.20  
    1.21    a_assoc:      "(a + b) + c = a + (b + c)"
    1.22    l_zero:       "0 + a = a"