--- 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