--- a/Correctness.thy	Fri Mar 17 14:57:30 2017 +0000
+++ b/Correctness.thy	Tue Apr 11 03:03:33 2017 +0800
@@ -1240,13 +1240,15 @@
 proof - 
   let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"
   from occs_le[of ?Q t] 
+  thm occs_le
   have "?L \<le> (1 + length t) - occs ?Q t" by simp
   also have "... \<le> ?R"
   proof -
+  thm actions_th_occs actions_split
     have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))
               \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")
     proof -
-      have "?L1 = length (actions_of {th} t)" using actions_split by arith
+      from actions_split have "?L1 = length (actions_of {th} t)" using actions_split by arith
       also have "... \<le> ?R1" using actions_th_occs by simp
       finally show ?thesis .
     qed            
@@ -1280,7 +1282,7 @@
     the particular environment in which it operates. In this particular case,
     we regard the @{term t} as the environment of thread @{term th}.
   *}
-  assumes finite_span: 
+  assumes finite_span:
           "th' \<in> blockers \<Longrightarrow>
                  (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> 
                                   \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"
@@ -1429,6 +1431,8 @@
   "length t - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)"
   using actions_split create_bc len_action_blockers by linarith
 
+thm actions_split
+
 end