diff -r 5faa1b59e870 -r 813e7257c7c3 prio/PrioG.thy
--- a/prio/PrioG.thy	Thu Feb 16 08:12:01 2012 +0000
+++ b/prio/PrioG.thy	Mon Feb 20 11:02:50 2012 +0000
@@ -361,7 +361,7 @@
   and "waiting s th cs1"
   and "waiting s th cs2"
   shows "cs1 = cs2"
-using waiting_unique_pre prems
+using waiting_unique_pre assms
 unfolding wq_def s_waiting_def
 by auto
 
@@ -371,7 +371,7 @@
   assumes "holding s th1 cs"
   and "holding s th2 cs"
   shows "th1 = th2"
-using prems
+using assms
 unfolding s_holding_def
 by auto
 
@@ -1204,7 +1204,7 @@
   and not_in: "th \<notin>  set rest"
   shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"
 proof -
-  from prems show ?thesis
+  from assms show ?thesis
     apply (auto simp:readys_def)
     apply(simp add:s_waiting_def[folded wq_def])
     apply (erule_tac x = csa in allE)
@@ -1354,7 +1354,7 @@
   and "wq s cs = []"
   shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
 proof -
-  from prems show ?thesis
+  from assms show ?thesis
   unfolding  holdents_def step_depend_p[OF vt] by auto
 qed
 
@@ -1364,7 +1364,7 @@
   and "wq s cs \<noteq> []"
   shows "holdents (P th cs#s) th = holdents s th"
 proof -
-  from prems show ?thesis
+  from assms show ?thesis
   unfolding  holdents_def step_depend_p[OF vt] by auto
 qed
 
@@ -1545,7 +1545,7 @@
       assume eq_e: "e = P thread cs"
         and is_runing: "thread \<in> runing s"
         and no_dep: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+"
-      from prems have vtp: "vt (P thread cs#s)" by auto
+      from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto
       show ?thesis 
       proof -
         { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
@@ -1650,7 +1650,7 @@
       qed
     next
       case (thread_V thread cs)
-      from prems have vtv: "vt (V thread cs # s)" by auto
+      from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto
       assume eq_e: "e = V thread cs"
         and is_runing: "thread \<in> runing s"
         and hold: "holding s thread cs"
@@ -1983,7 +1983,7 @@
       case (thread_P thread cs)
       assume eq_e: "e = P thread cs"
       and is_runing: "thread \<in> runing s"
-      from prems have vtp: "vt (P thread cs#s)" by auto
+      from assms thread_P ih vt stp thread_P have vtp: "vt (P thread cs#s)" by auto
       have neq_th: "th \<noteq> thread" 
       proof -
         from not_in eq_e have "th \<notin> threads s" by simp
@@ -2011,7 +2011,7 @@
           by (simp add:runing_def readys_def)
         ultimately show ?thesis by auto
       qed
-      from prems have vtv: "vt (V thread cs#s)" by auto
+      from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto
       from hold obtain rest 
         where eq_wq: "wq s cs = thread # rest"
         by (case_tac "wq s cs", auto simp: wq_def s_holding_def)