--- 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)