# HG changeset patch
# User paulson
# Date 880023339 -3600
# Node ID c539e702e1d2bf448c4d7fe3ec0ce354ad45b13f
# Parent  b9ce25073cc04fa80a348e87847fe25b044ebc81
Now uses induct_tac

diff -r b9ce25073cc0 -r c539e702e1d2 src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Thu Nov 20 11:54:31 1997 +0100
+++ b/src/HOL/ex/NatSum.ML	Thu Nov 20 11:55:39 1997 +0100
@@ -13,7 +13,7 @@
 (*The sum of the first n positive integers equals n(n+1)/2.*)
 goal NatSum.thy "2*sum (%i. i) (Suc n) = n*Suc(n)";
 by (Simp_tac 1);
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "sum_of_naturals";
@@ -21,7 +21,7 @@
 goal NatSum.thy
   "Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
 by (Simp_tac 1);
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "sum_of_squares";
@@ -29,14 +29,14 @@
 goal NatSum.thy
   "Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
 by (Simp_tac 1);
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 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 (induct_tac "n" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "sum_of_odds";