| changeset 30082 | 43c5b7bfc791 |
| parent 30042 | 31039ee583fa |
| child 30198 | 922f944f03b2 |
--- a/src/HOL/RealDef.thy Tue Feb 24 11:10:05 2009 -0800 +++ b/src/HOL/RealDef.thy Tue Feb 24 11:12:58 2009 -0800 @@ -705,6 +705,9 @@ lemma real_of_nat_zero [simp]: "real (0::nat) = 0" by (simp add: real_of_nat_def) +lemma real_of_nat_1 [simp]: "real (1::nat) = 1" +by (simp add: real_of_nat_def) + lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)" by (simp add: real_of_nat_def)