| changeset 23438 | dd824e86fa8a |
| parent 23431 | 25ca91279a9b |
| child 23477 | f4b83f03cac9 |
--- a/src/HOL/Real/RealDef.thy Wed Jun 20 17:02:57 2007 +0200 +++ b/src/HOL/Real/RealDef.thy Wed Jun 20 17:28:55 2007 +0200 @@ -739,7 +739,7 @@ by (simp add: real_of_nat_def) lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n" -by (simp add: add: real_of_nat_def) +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)