diff -r f1e6071a4613 -r 24199eb2c423 prio/PrioG.thy
--- a/prio/PrioG.thy	Tue Jan 24 00:34:52 2012 +0000
+++ b/prio/PrioG.thy	Fri Jan 27 13:50:02 2012 +0000
@@ -1,5 +1,5 @@
 theory PrioG
-imports PrioGDef
+imports PrioGDef 
 begin
 
 lemma runing_ready: "runing s \<subseteq> readys s"
@@ -349,6 +349,7 @@
 qed
 
 lemma waiting_unique:
+  fixes s cs1 cs2
   assumes "vt step s"
   and "waiting s th cs1"
   and "waiting s th cs2"
@@ -359,7 +360,7 @@
     by (auto simp add:s_waiting_def)
 qed
 
-lemma holded_unique:
+lemma held_unique:
   assumes "vt step s"
   and "holding s th1 cs"
   and "holding s th2 cs"