# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1412760614 -3600
# Node ID 378077bab5d24e367c65bf6552d932cc6f19665c
# Parent  51444f205b5bde1b2ef9f958e14a1f4bd0914c56
added done to the proof.

diff -r 51444f205b5b -r 378077bab5d2 thys/CountSnoc.thy
--- a/thys/CountSnoc.thy	Wed Oct 08 10:28:19 2014 +0100
+++ b/thys/CountSnoc.thy	Wed Oct 08 10:30:14 2014 +0100
@@ -26,6 +26,7 @@
 lemma count1: "count_list n(xs @ ys) = count_list n xs + count_list n ys"
 apply(induct xs)
 apply(auto)
+done