--- a/src/HOL/Nat.thy Tue May 11 14:00:02 2004 +0200
+++ b/src/HOL/Nat.thy Tue May 11 20:11:08 2004 +0200
@@ -712,8 +712,8 @@
by (induct m) (simp_all add: add_mult_distrib)
-text{*The Naturals Form A Semiring*}
-instance nat :: semiring
+text{*The Naturals Form A comm_semiring_1_cancel*}
+instance nat :: comm_semiring_1_cancel
proof
fix i j k :: nat
show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
@@ -760,8 +760,8 @@
done
-text{*The Naturals Form an Ordered Semiring*}
-instance nat :: ordered_semiring
+text{*The Naturals Form an Ordered comm_semiring_1_cancel*}
+instance nat :: ordered_semidom
proof
fix i j k :: nat
show "0 < (1::nat)" by simp