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