--- a/thys/MyFirst.thy	Mon Oct 06 16:42:52 2014 +0100
+++ b/thys/MyFirst.thy	Tue Oct 07 12:33:27 2014 +0100
@@ -48,6 +48,9 @@
 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)
@@ -61,6 +64,7 @@
 
 lemma add_Suc: "add m (Suc n) = Suc (add m n)"
 apply(induct m)
+apply(metis add.simps(1))
 apply(auto)
 done