# HG changeset patch
# User fahadausaf <fahad.ausaf@icloud.com>
# Date 1412610172 -3600
# Node ID 893f0314a88b71403787834b3f11a6ae0c94ad37
# Parent  c11651bbebf59ac1ccd600ca4dccd79aed2dc850
add

diff -r c11651bbebf5 -r 893f0314a88b thys/MyFirst.thy
--- a/thys/MyFirst.thy	Mon Oct 06 15:24:41 2014 +0100
+++ b/thys/MyFirst.thy	Mon Oct 06 16:42:52 2014 +0100
@@ -48,9 +48,6 @@
 apply(auto)
 done
 
-value "add 2 3"
-
-
 (**commutative-associative**)
 lemma add_04: "add m (add n k) = add (add m n) k"
 apply(induct m)
@@ -58,10 +55,14 @@
 done
 
 lemma add_zero: "add n 0 = n"
-sorry
+apply(induct n)
+apply(auto)
+done
 
 lemma add_Suc: "add m (Suc n) = Suc (add m n)"
-sorry
+apply(induct m)
+apply(auto)
+done
 
 lemma add_comm: "add m n = add n m"
 apply(induct m)