src/HOL/ex/ThreeDivides.thy
changeset 19114 dfe6ace301c3
parent 19106 6e6b5b1fdc06
child 19279 48b527d0331b
     1.1 --- a/src/HOL/ex/ThreeDivides.thy	Mon Feb 20 16:23:38 2006 +0100
     1.2 +++ b/src/HOL/ex/ThreeDivides.thy	Mon Feb 20 21:51:50 2006 +0100
     1.3 @@ -207,7 +207,7 @@
     1.4           (simp add: atLeast0LessThan)
     1.5      also have
     1.6        "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
     1.7 -      by (simp add: setsum_rmv_upt cdef)
     1.8 +      by (simp add: setsum_head_upt cdef)
     1.9      also note `Suc nd = nlen m`
    1.10      finally
    1.11      show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .