diff -r 289e362f7a76 -r 389ef8b1959c Correctness.thy
--- a/Correctness.thy	Fri Oct 07 14:05:08 2016 +0100
+++ b/Correctness.thy	Fri Oct 07 21:15:35 2016 +0100
@@ -501,13 +501,17 @@
   precedence in the whole system.
 *}
 lemma running_preced_inversion:
-  assumes running': "th' \<in> running (t@s)"
-  shows "cp (t@s) th' = preced th s" (is "?L = ?R")
+  assumes running': "th' \<in> running (t @ s)"
+  shows "cp (t @ s) th' = preced th s"
 proof -
-  have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
-      by (unfold running_def, auto)
-  also have "\<dots> = ?R"
-      by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) 
+  have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" using assms
+      unfolding running_def by simp
+  also have "... =  Max (cp (t @ s) ` threads (t @ s))"
+      using vat_t.max_cp_readys_threads .
+  also have "... = cp (t @ s) th"
+      using th_cp_max .
+  also have "\<dots> = preced th s"
+      using th_cp_preced .
   finally show ?thesis .
 qed