Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Real/RealDef.thy
changeset 23431 25ca91279a9b
parent 23289 0cf371d943b1
child 23438 dd824e86fa8a 
--- a/src/HOL/Real/RealDef.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -712,7 +712,7 @@
 by (simp add: real_of_nat_def del: of_nat_Suc)
 
 lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
-by (simp add: real_of_nat_def)
+by (simp add: real_of_nat_def of_nat_mult)
 
 lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 
     (SUM x:A. real(f x))"
isabelle