src/HOL/Nat.thy
changeset 59833 ab828c2c5d67
parent 59816 034b13f4efae
child 60175 831ddb69db9b
     1.1 --- a/src/HOL/Nat.thy	Sat Mar 28 20:43:19 2015 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sat Mar 28 21:32:48 2015 +0100
     1.3 @@ -783,18 +783,13 @@
     1.4  apply (simp_all add: add_less_mono)
     1.5  done
     1.6  
     1.7 -text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
     1.8 +text{*The naturals form an ordered @{text semidom}*}
     1.9  instance nat :: linordered_semidom
    1.10  proof
    1.11    show "0 < (1::nat)" by simp
    1.12    show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
    1.13    show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
    1.14 -qed
    1.15 -
    1.16 -instance nat :: semiring_no_zero_divisors
    1.17 -proof
    1.18 -  fix m n :: nat
    1.19 -  show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
    1.20 +  show "\<And>m n :: nat. m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
    1.21  qed
    1.22  
    1.23