--- a/Correctness.thy	Thu Jan 28 21:14:17 2016 +0800
+++ b/Correctness.thy	Fri Jan 29 09:46:07 2016 +0800
@@ -694,7 +694,7 @@
   characterisationof the blocking thread @{text "th'"}:
 
 *}
-
+                  
 lemma runing_inversion: (* ddd, one of the main lemmas to present *)
   assumes runing': "th' \<in> runing (t@s)"
   and neq_th: "th' \<noteq> th"