| changeset 44766 | d4d33a4d7548 |
| parent 44350 | 63cddfbc5a09 |
| child 44822 | 2690b6de5021 |
--- a/src/HOL/RealDef.thy Tue Sep 06 16:30:39 2011 -0700 +++ b/src/HOL/RealDef.thy Tue Sep 06 19:03:41 2011 -0700 @@ -1412,7 +1412,7 @@ by (insert real_of_nat_div2 [of n x], simp) lemma real_of_int_real_of_nat: "real (int n) = real n" -by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat) +by (simp add: real_of_nat_def real_of_int_def) lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n" by (simp add: real_of_int_def real_of_nat_def)