thys/MyFirst.thy
changeset 19 66c9c06c0f0e
parent 17 a5427713eef4
child 20 c11651bbebf5
equal deleted inserted replaced
18:8c9349065477 19:66c9c06c0f0e
   102 (**
   102 (**
   103 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where
   103 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where
   104 "count  "
   104 "count  "
   105 **)
   105 **)
   106 
   106 
       
   107 fun sum :: "nat \<Rightarrow> nat" where
       
   108 "sum n = 0 + \<dots> + n"
       
   109 (* prove n = n * (n + 1) div 2  *)
   107 
   110 
   108 
   111 
   109 
   112 
   110 
   113 
   111 
   114 
   112 
   115 
   113 
   116 
   114 
   117 
   115 
   118 
       
   119 
       
   120