
diff -r 789ade899a53 -r a2a7f65f538a thys/CountSnoc.thy
--- a/thys/CountSnoc.thy	Tue Oct 07 16:17:23 2014 +0100
+++ b/thys/CountSnoc.thy	Tue Oct 07 18:43:29 2014 +0100
@@ -22,6 +22,11 @@
 value "count_list (1::nat) [1,1,1]"
 value "count_list (1::nat) [2,2,2]"
 value "count_list (2::nat) [2,2,1]"
+
+lemma count1: "count_list n(xs @ ys) = count_list n xs + count_list n ys"
+apply(induct xs)
+apply(auto)
+ 
  
 
 




