--- a/Correctness.thy	Thu Jan 28 14:26:10 2016 +0000
+++ b/Correctness.thy	Thu Jan 28 14:57:36 2016 +0000
@@ -802,7 +802,7 @@
 *}
 
 lemma live: "runing (t @ s) \<noteq> {}"
-proof(cases "th \<in> runing (t@s)") 
+proof(cases "th \<in> runing (t @ s)") 
   case True thus ?thesis by auto
 next
   case False