src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Sun Feb 22 11:30:57 2009 +0100
+++ b/src/HOL/Nat.thy	Sun Feb 22 17:25:28 2009 +0100
@@ -735,6 +735,11 @@
   show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
 qed
 
+instance nat :: no_zero_divisors
+proof
+  fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
+qed
+
 lemma nat_mult_1: "(1::nat) * n = n"
 by simp