# HG changeset patch
# User fahadausaf <fahad.ausaf@icloud.com>
# Date 1412601733 -3600
# Node ID 66c9c06c0f0e3f0d8d0d22e68aec1d355bba3f54
# Parent  8c9349065477142c6ce563673e20e21cfe6756d1
abc

diff -r 8c9349065477 -r 66c9c06c0f0e thys/MyFirst.thy
--- 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 @@
 
 
 
+
+