src/HOL/Real/RealDef.thy
changeset 23431 25ca91279a9b
parent 23289 0cf371d943b1
child 23438 dd824e86fa8a
     1.1 --- a/src/HOL/Real/RealDef.thy	Wed Jun 20 05:06:56 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Wed Jun 20 05:18:39 2007 +0200
     1.3 @@ -712,7 +712,7 @@
     1.4  by (simp add: real_of_nat_def del: of_nat_Suc)
     1.5  
     1.6  lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
     1.7 -by (simp add: real_of_nat_def)
     1.8 +by (simp add: real_of_nat_def of_nat_mult)
     1.9  
    1.10  lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 
    1.11      (SUM x:A. real(f x))"