--- 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)
--- a/src/HOL/Nat.thy Wed Jun 06 16:42:39 2007 +0200
+++ b/src/HOL/Nat.thy Wed Jun 06 17:00:09 2007 +0200
@@ -1292,9 +1292,9 @@
subsection{*Embedding of the Naturals into any
- @{text semiring_1_cancel}: @{term of_nat}*}
+ @{text semiring_1}: @{term of_nat}*}
-consts of_nat :: "nat => 'a::semiring_1_cancel"
+consts of_nat :: "nat => 'a::semiring_1"
primrec
of_nat_0: "of_nat 0 = 0"
@@ -1353,7 +1353,7 @@
lemma of_nat_le_0_iff [simp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
by (rule of_nat_le_iff [of _ 0, simplified])
-text{*The ordering on the @{text semiring_1_cancel} is necessary
+text{*The ordering on the @{text semiring_1} is necessary
to exclude the possibility of a finite field, which indeed wraps back to
zero.*}
lemma of_nat_eq_iff [simp]: