--- a/thys/MyFirst.thy	Mon Oct 06 13:44:27 2014 +0100
+++ b/thys/MyFirst.thy	Mon Oct 06 14:22:13 2014 +0100
@@ -104,6 +104,9 @@
 "count  "
 **)
 
+fun sum :: "nat \<Rightarrow> nat" where
+"sum n = 0 + \<dots> + n"
+(* prove n = n * (n + 1) div 2  *)
 
 
 
@@ -113,3 +116,5 @@
 
 
 
+
+