1.1 --- a/src/HOL/Nat.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -712,8 +712,8 @@
     1.4    by (induct m) (simp_all add: add_mult_distrib)
     1.5  
     1.6  
     1.7 -text{*The Naturals Form A Semiring*}
     1.8 -instance nat :: semiring
     1.9 +text{*The Naturals Form A comm_semiring_1_cancel*}
    1.10 +instance nat :: comm_semiring_1_cancel
    1.11  proof
    1.12    fix i j k :: nat
    1.13    show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
    1.14 @@ -760,8 +760,8 @@
    1.15    done
    1.16  
    1.17  
    1.18 -text{*The Naturals Form an Ordered Semiring*}
    1.19 -instance nat :: ordered_semiring
    1.20 +text{*The Naturals Form an Ordered comm_semiring_1_cancel*}
    1.21 +instance nat :: ordered_semidom
    1.22  proof
    1.23    fix i j k :: nat
    1.24    show "0 < (1::nat)" by simp