Mercurial Mercurial > hg > regexp / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
prio/PrioG.thy
changeset 264 24199eb2c423
parent 262 4190df6f4488
child 287 440382eb6427 
--- 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"
regexp