# HG changeset patch
# User huffman
# Date 1181142009 -7200
# Node ID a70934b63910c7edda3d03efc739dabee3453fa5
# Parent  339cdc29b0bc3ca61e6f047742eee35ecfb63d3c
generalize of_nat and related constants to class semiring_1

diff -r 339cdc29b0bc -r a70934b63910 src/HOL/IntDef.thy
--- 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)
diff -r 339cdc29b0bc -r a70934b63910 src/HOL/Nat.thy
--- 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]: