--- a/Correctness.thy	Fri Apr 21 20:17:13 2017 +0800
+++ b/Correctness.thy	Tue Apr 25 14:05:57 2017 +0100
@@ -1287,6 +1287,9 @@
 
 definition "up_to s t = map (\<lambda> t'. t'@s) (postfixes t)"
 
+
+
+
 definition "occs' Q tt = length (filter Q (postfixes tt))"
 
 lemma occs'_nil [simp]: "occs' Q [] = 0"