--- a/prio/CpsG.thy	Mon Feb 13 10:57:47 2012 +0000
+++ b/prio/CpsG.thy	Mon Feb 13 15:35:08 2012 +0000
@@ -245,12 +245,15 @@
 qed
 
 definition child :: "state \<Rightarrow> (node \<times> node) set"
-  where "child s =
+  where "child s \<equiv>
             {(Th th', Th th) | th th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
 
 definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
-  where "children s th = {th'. (Th th', Th th) \<in> child s}"
+  where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"
 
+lemma children_def2:
+  "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
+unfolding child_def children_def by simp
 
 lemma children_dependents: "children s th \<subseteq> dependents (wq s) th"
   by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
@@ -1004,7 +1007,7 @@
 begin
 
 lemma depend_s:
-  "depend s = (depend s' - {(Cs cs, Th th)} - {(Th th', Cs cs)}) \<union>
+  "depend s = (depend s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
                                          {(Cs cs, Th th')}"
 proof -
   from step_depend_v[OF vt_s[unfolded s_def], folded s_def]