diff -r 704fd8749dad -r ca4ddf26a7c7 Correctness.thy
--- a/Correctness.thy	Thu Sep 21 14:33:13 2017 +0100
+++ b/Correctness.thy	Fri Sep 22 03:08:30 2017 +0100
@@ -2,8 +2,6 @@
 imports PIPBasics
 begin
 
-(* hg cat -r 176 Correctness.thy *)
-
 lemma actions_of_len_cons [iff]: 
     "length (actions_of ts (e#t)) \<le> length ((actions_of ts t)) + 1"
       by  (unfold actions_of_def, simp)
@@ -88,8 +86,8 @@
   by (unfold highest, rule Max_ge, 
         auto simp:threads_s finite_threads)
   moreover have "?R \<le> ?L"
-    by (unfold vat_s.cp_rec, rule Max_ge, 
-        auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)
+    apply(subst vat_s.cp_rec)
+    using cp_rec le_cp by auto  
   ultimately show ?thesis by auto
 qed
 
@@ -843,8 +841,8 @@
         show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
       next
         show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)"
-          by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in 
-                the_thread.simps vat_t.subtree_tRAG_thread)
+          by (metis DiffI Diff_eq_empty_iff empty_iff readys_threads 
+              subtree_tG_tRAG th'_in vat_t.subtree_tG_thread)
       next
         show "th \<in> the_thread ` subtree (tRAG (t @ s)) (Th th')"
         proof -
@@ -1313,8 +1311,7 @@
         by (unfold occs'_def, simp)
 
 lemma occs'_cons [simp]: 
-  shows "occs' Q (x#xs) = (if Q xs then 1 + occs' Q xs else occs' Q xs)"
-  using assms   
+  shows "occs' Q (x#xs) = (if Q xs then 1 + occs' Q xs else occs' Q xs)"   
   by (unfold occs'_def, simp)
 
 lemma occs_len': "occs' Q t + occs' (\<lambda>e. \<not> Q e) t = length t"
@@ -1644,7 +1641,7 @@
   from len_actions_of_sigma[OF finite_blockers]
   have "?L  = (\<Sum>th'\<in>blockers. length (actions_of {th'} t))" by simp
   also have "... \<le> ?R"
-    by (rule Groups_Big.setsum_mono, insert le_span, auto)
+    by (simp add: le_span sum_mono)
   finally show ?thesis .
 qed