--- a/thys/CountSnoc.thy	Sun Oct 26 16:42:28 2014 +0000
+++ b/thys/CountSnoc.thy	Tue Oct 28 15:36:14 2014 +0000
@@ -23,11 +23,15 @@
 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"
+lemma count1: "count_list n (xs @ ys) = count_list n xs + count_list n ys"
 apply(induct xs)
 apply(auto)
 done
  
+thm count1
+thm refl
+thm conjI[OF refl[of "a"] refl[of "b"]]
+thm conjI[OF conjI]