src/HOL/ex/ThreeDivides.thy
changeset 19736 d8d0f8f51d69
parent 19279 48b527d0331b
child 20503 503ac4c5ef91
     1.1 --- a/src/HOL/ex/ThreeDivides.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/ex/ThreeDivides.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -155,9 +155,9 @@
     1.4  text {* The function @{text "sumdig"} returns the sum of all digits in
     1.5  some number n. *}
     1.6  
     1.7 -constdefs 
     1.8 +definition
     1.9    sumdig :: "nat \<Rightarrow> nat"
    1.10 -  "sumdig n \<equiv> \<Sum>x < nlen n. n div 10^x mod 10"
    1.11 +  "sumdig n = (\<Sum>x < nlen n. n div 10^x mod 10)"
    1.12  
    1.13  text {* Some properties of these functions follow. *}
    1.14