src/HOL/Nat.thy
changeset 30056 0a35bee25c20
parent 29879 4425849f5db7
child 30079 293b896b9c25
     1.1 --- a/src/HOL/Nat.thy	Sun Feb 22 11:30:57 2009 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sun Feb 22 17:25:28 2009 +0100
     1.3 @@ -735,6 +735,11 @@
     1.4    show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
     1.5  qed
     1.6  
     1.7 +instance nat :: no_zero_divisors
     1.8 +proof
     1.9 +  fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
    1.10 +qed
    1.11 +
    1.12  lemma nat_mult_1: "(1::nat) * n = n"
    1.13  by simp
    1.14