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/ex/Sum_of_Powers.thy
changeset 61694 6571c78c9667
parent 61649 268d88ec9087
child 63367 6c731c8b7f03 
--- a/src/HOL/ex/Sum_of_Powers.thy	Tue Nov 17 12:01:19 2015 +0100
+++ b/src/HOL/ex/Sum_of_Powers.thy	Tue Nov 17 12:32:08 2015 +0000
@@ -189,7 +189,7 @@
     by (auto simp add: sum_of_powers)
   also have "... = ((n ^ 2 + n) / 2) ^ 2"
     by (simp add: unroll algebra_simps power2_eq_square power4_eq power3_eq_cube)
-  finally show ?thesis by simp
+  finally show ?thesis by (simp add: power_divide)
 qed
                        
 lemma sum_of_cubes_nat: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 div 4"
isabelle