# HG changeset patch
# User kleing
# Date 1140468710 -3600
# Node ID dfe6ace301c33fdb47eae8c3f8de6a9e85d2b4d9
# Parent  2cb4559782f4733b40c1793f6683f076ac55a331
fixed

diff -r 2cb4559782f4 -r dfe6ace301c3 src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Mon Feb 20 16:23:38 2006 +0100
+++ b/src/HOL/ex/ThreeDivides.thy	Mon Feb 20 21:51:50 2006 +0100
@@ -207,7 +207,7 @@
          (simp add: atLeast0LessThan)
     also have
       "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
-      by (simp add: setsum_rmv_upt cdef)
+      by (simp add: setsum_head_upt cdef)
     also note `Suc nd = nlen m`
     finally
     show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .