--- a/src/HOL/Nat.thy Fri Nov 21 11:15:40 2003 +0100
+++ b/src/HOL/Nat.thy Mon Nov 24 15:33:07 2003 +0100
@@ -992,7 +992,9 @@
lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
by (drule mult_less_mono2) (simp_all add: mult_commute)
-lemma zero_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
+text{*Differs from the standard @{text zero_less_mult_iff} in that
+ there are no negative numbers.*}
+lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
apply (induct m)
apply (case_tac [2] n, simp_all)
done