--- a/src/HOL/IntDef.thy Wed Jun 06 16:42:39 2007 +0200
+++ b/src/HOL/IntDef.thy Wed Jun 06 17:00:09 2007 +0200
@@ -521,7 +521,7 @@
[code inline]: "neg Z \<longleftrightarrow> Z < 0"
definition (*for simplifying equalities*)
- iszero :: "'a\<Colon>comm_semiring_1_cancel \<Rightarrow> bool"
+ iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
where
"iszero z \<longleftrightarrow> z = 0"
@@ -561,7 +561,7 @@
subsection{*The Set of Natural Numbers*}
constdefs
- Nats :: "'a::semiring_1_cancel set"
+ Nats :: "'a::semiring_1 set"
"Nats == range of_nat"
notation (xsymbols)