--- a/Correctness.thy	Wed Feb 03 14:37:35 2016 +0000
+++ b/Correctness.thy	Thu Feb 04 00:43:05 2016 +0000
@@ -406,7 +406,7 @@
       have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = 
             the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and>
                             (\<exists> th'. n = Th th')}"
-      by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps)
+        by (force)
       moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) 
       ultimately show ?thesis by simp
     qed

--- a/Implementation.thy	Wed Feb 03 14:37:35 2016 +0000
+++ b/Implementation.thy	Thu Feb 04 00:43:05 2016 +0000
@@ -1,10 +1,11 @@
+theory Implementation
+imports PIPBasics
+begin
+
 section {*
   This file contains lemmas used to guide the recalculation of current precedence 
   after every system call (or system operation)
 *}
-theory Implementation
-imports PIPBasics
-begin
 
 text {* (* ddd *)
   One beauty of our modelling is that we follow the definitional extension tradition of HOL.

--- a/PIPBasics.thy	Wed Feb 03 14:37:35 2016 +0000
+++ b/PIPBasics.thy	Thu Feb 04 00:43:05 2016 +0000
@@ -211,7 +211,7 @@
   obtains rest where "wq s cs = th#rest"
 proof -
   from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest"
-    by (meson list.set_cases)
+    by (metis empty_iff list.exhaust list.set(1))
   have "th' = th"
   proof(rule ccontr)
     assume "th' \<noteq> th"
@@ -1254,8 +1254,7 @@
   moreover hence "t \<noteq> th" using assms neq_t_th by blast 
   moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) 
   ultimately have "waiting s t cs"
-    by (metis cs_waiting_def list.distinct(2) list.sel(1) 
-                list.set_sel(2) rest_def waiting_eq wq_s_cs)  
+    by (metis cs_waiting_def insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs)
   show ?thesis using that(2)
   using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto   
 qed
@@ -1594,9 +1593,9 @@
   assumes "waiting s th' cs'"
   shows "waiting (e#s) th' cs'"
   using assms
-  by (metis cs_waiting_def hd_append2 list.sel(1) list.set_intros(2) 
-      rotate1.simps(2) self_append_conv2 set_rotate1 
-        th_not_in_wq waiting_eq wq_es_cs wq_neq_simp)
+  unfolding th_not_in_wq waiting_eq cs_waiting_def
+  by (metis append_is_Nil_conv butlast_snoc hd_append2 in_set_butlastD 
+    list.distinct(1) split_list wq_es_cs wq_neq_simp)
 
 lemma holding_kept:
   assumes "holding s th' cs'"
@@ -1748,8 +1747,9 @@
 next
   case True
   with assms show ?thesis
-  by (metis cs_holding_def holding_eq list.sel(1) list.set_intros(1) that 
-        wq_es_cs' wq_s_cs) 
+    using event.inject(3) holder_def is_p s_holding_def s_waiting_def that 
+      waiting_es_th_cs wq_def wq_es_cs' wq_in_inv
+    by(force)
 qed
 
 lemma waiting_esE: