src/HOL/IntDef.thy
changeset 23276 a70934b63910
parent 23164 69e55066dbca
child 23282 dfc459989d24
     1.1 --- a/src/HOL/IntDef.thy	Wed Jun 06 16:42:39 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Wed Jun 06 17:00:09 2007 +0200
     1.3 @@ -521,7 +521,7 @@
     1.4    [code inline]: "neg Z \<longleftrightarrow> Z < 0"
     1.5  
     1.6  definition (*for simplifying equalities*)
     1.7 -  iszero :: "'a\<Colon>comm_semiring_1_cancel \<Rightarrow> bool"
     1.8 +  iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
     1.9  where
    1.10    "iszero z \<longleftrightarrow> z = 0"
    1.11  
    1.12 @@ -561,7 +561,7 @@
    1.13  subsection{*The Set of Natural Numbers*}
    1.14  
    1.15  constdefs
    1.16 -  Nats  :: "'a::semiring_1_cancel set"
    1.17 +  Nats  :: "'a::semiring_1 set"
    1.18    "Nats == range of_nat"
    1.19  
    1.20  notation (xsymbols)