# HG changeset patch
# User paulson
# Date 977234774 -3600
# Node ID dc5e984dfe1337eed59f1169ae0af825a74a07e5
# Parent  ec197510165a5b73c93ed0ef014ecaa815e926f0
cancel-factor simproc allows a shorter proof

diff -r ec197510165a -r dc5e984dfe13 src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Tue Dec 19 13:06:49 2000 +0100
+++ b/src/HOL/ex/NatSum.ML	Tue Dec 19 15:06:14 2000 +0100
@@ -93,8 +93,4 @@
 Goal "0<k ==> (k-1) * setsum (%i. k^i) (lessThan n) = k^n - 1";
 by (induct_tac "n" 1);
 by Auto_tac;
-by (subgoal_tac "1*k^n <= k * k^n" 1);
-by (Asm_full_simp_tac 1);
-by (rtac mult_le_mono1 1);
-by Auto_tac;
 qed "sum_of_powers";