--- a/PIPDefs.thy	Fri Apr 15 14:44:09 2016 +0100
+++ b/PIPDefs.thy	Thu Jun 02 13:15:03 2016 +0100
@@ -38,12 +38,14 @@
   V thread cs | -- {* Thread @{text "thread"}  releasing critical resource @{text "cs"}. *}
   Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *}
 
-fun actor :: "event \<Rightarrow> thread" where
-  "actor (Create th pty) = th" |
+fun actor  where
   "actor (Exit th) = th" |
   "actor (P th cs) = th" |
   "actor (V th cs) = th" |
-  "actor (Set th pty) = th"
+  "actor (Set th pty) = th" |
+  "actor (Create th prio) = th"
+
+definition "actions_of ths s = filter (\<lambda> e. actor e \<in> ths) s"
 
 fun isCreate :: "event \<Rightarrow> bool" where
   "isCreate (Create th pty) = True" |