Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/ThreeDivides.thy
changeset 28071 6ab5b4595f64
parent 23373 ead82c82da9e
child 29974 ca93255656a5 
--- a/src/HOL/ex/ThreeDivides.thy	Mon Sep 01 19:17:37 2008 +0200
+++ b/src/HOL/ex/ThreeDivides.thy	Mon Sep 01 19:17:47 2008 +0200
@@ -210,7 +210,7 @@
          (simp add: atLeast0LessThan)
     also have
       "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
-      by (simp add: setsum_head_upt cdef)
+      by (simp add: atLeast0LessThan[symmetric] setsum_head_upt_Suc cdef)
     also note `Suc nd = nlen m`
     finally
     show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .
isabelle