diff -r f04b33ce250f -r a4dc62a46ee4 ex/NatSum.ML
--- a/ex/NatSum.ML	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title: 	HOL/ex/natsum.ML
-    ID:         $Id$
-    Author: 	Tobias Nipkow
-    Copyright   1994 TU Muenchen
-
-Summing natural numbers, squares and cubes. Could be continued...
-*)
-
-val natsum_ss = arith_ss addsimps
-  ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
-
-(*The sum of the first n positive integers equals n(n+1)/2.*)
-goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
-by (simp_tac natsum_ss 1);
-by (nat_ind_tac "n" 1);
-by (simp_tac natsum_ss 1);
-by (asm_simp_tac natsum_ss 1);
-qed "sum_of_naturals";
-
-goal NatSum.thy
-  "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum(%i.i*i,Suc(n)) = \
-\  n*Suc(n)*Suc(Suc(Suc(0))*n)";
-by (simp_tac natsum_ss 1);
-by (nat_ind_tac "n" 1);
-by (simp_tac natsum_ss 1);
-by (asm_simp_tac natsum_ss 1);
-qed "sum_of_squares";
-
-goal NatSum.thy
-  "Suc(Suc(Suc(Suc(0))))*sum(%i.i*i*i,Suc(n)) = n*n*Suc(n)*Suc(n)";
-by (simp_tac natsum_ss 1);
-by (nat_ind_tac "n" 1);
-by (simp_tac natsum_ss 1);
-by (asm_simp_tac natsum_ss 1);
-qed "sum_of_cubes";
-
-(*The sum of the first n odd numbers equals n squared.*)
-goal NatSum.thy "sum(%i.Suc(i+i), n) = n*n";
-by (nat_ind_tac "n" 1);
-by (simp_tac natsum_ss 1);
-by (asm_simp_tac natsum_ss 1);
-qed "sum_of_odds";
-