merged
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 28 Jan 2016 14:57:36 +0000
changeset 96 4805c6333fef
parent 95 8d2cc27f45f3
child 97 c7ba70dc49bd
merged
Correctness.thy
--- 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