| changeset 21404 | eb85850d3eb7 |
| parent 20503 | 503ac4c5ef91 |
| child 23219 | 87ad6e8a5f2c |
--- a/src/HOL/ex/ThreeDivides.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/ex/ThreeDivides.thy Fri Nov 17 02:20:03 2006 +0100 @@ -156,7 +156,7 @@ some number n. *} definition - sumdig :: "nat \<Rightarrow> nat" + sumdig :: "nat \<Rightarrow> nat" where "sumdig n = (\<Sum>x < nlen n. n div 10^x mod 10)" text {* Some properties of these functions follow. *}