# HG changeset patch
# User paulson
# Date 901636592 -7200
# Node ID a3f26b19cd7e642560b43178c47bc1c5da062c41
# Parent  6023540393069261b91f68d3ee99e68122296574
Tidied

diff -r 602354039306 -r a3f26b19cd7e src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Tue Jul 28 16:33:43 1998 +0200
+++ b/src/HOL/ex/NatSum.ML	Tue Jul 28 16:36:32 1998 +0200
@@ -19,16 +19,14 @@
 by (Asm_simp_tac 1);
 qed "sum_of_naturals";
 
-Goal
-  "Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
+Goal "Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
 by (Simp_tac 1);
 by (induct_tac "n" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "sum_of_squares";
 
-Goal
-  "Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
+Goal "Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
 by (Simp_tac 1);
 by (induct_tac "n" 1);
 by (Simp_tac 1);