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/NumberTheory/Fib.thy
changeset 11786 51ce34ef5113
parent 11704 3c50a2cd6f00
child 11868 56db9f3a6b3e 
--- a/src/HOL/NumberTheory/Fib.thy	Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Mon Oct 15 20:42:06 2001 +0200
@@ -118,7 +118,7 @@
   done
 
 lemma fib_mult_eq_setsum:
-    "fib (Suc n) * fib n = setsum (\<lambda>k. fib k * fib k) (atMost n)"
+    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   apply (induct n rule: fib.induct)
     apply (auto simp add: atMost_Suc fib.Suc_Suc)
   apply (simp add: add_mult_distrib add_mult_distrib2)
isabelle