src/HOL/Real/RealDef.thy
changeset 25162 ad4d5365d9d8
parent 25140 273772abbea2
child 25303 0699e20feabd
     1.1 --- a/src/HOL/Real/RealDef.thy	Tue Oct 23 22:48:25 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Tue Oct 23 23:27:23 2007 +0200
     1.3 @@ -746,7 +746,7 @@
     1.4  lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
     1.5  by (simp add: add: real_of_nat_def of_nat_diff)
     1.6  
     1.7 -lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (n \<noteq> 0)"
     1.8 +lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
     1.9  by (auto simp: real_of_nat_def)
    1.10  
    1.11  lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"