--- a/thys/MyFirst.thy	Mon Oct 06 11:46:23 2014 +0100
+++ b/thys/MyFirst.thy	Mon Oct 06 12:00:46 2014 +0100
@@ -50,6 +50,7 @@
 
 value "add 2 3"
 
+(**commutative-associative**)
 lemma add_04: "add m (add n k) = add k (add m n)"
 apply(induct)
 apply(auto)