--- a/src/HOL/Real/RealDef.thy Sun Oct 21 19:32:19 2007 +0200
+++ b/src/HOL/Real/RealDef.thy Sun Oct 21 22:33:35 2007 +0200
@@ -746,8 +746,8 @@
lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
by (simp add: add: real_of_nat_def of_nat_diff)
-lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
-by (simp add: add: real_of_nat_def)
+lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (n \<noteq> 0)"
+by (auto simp: real_of_nat_def)
lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
by (simp add: add: real_of_nat_def)
@@ -755,7 +755,7 @@
lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
by (simp add: add: real_of_nat_def)
-lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)"
+lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat))"
by (simp add: add: real_of_nat_def)
lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"