src/HOL/UNITY/Deadlock.ML

     Misra, "A Logic for Concurrent Programming", 1994
 *)
 
 (*Trivial, two-process case*)
 Goalw [constrains_def, stable_def]
-    "[| F : constrains (A Int B) A;  F : constrains (B Int A) B |] \
+    "[| F : (A Int B) co A;  F : (B Int A) co B |] \
 \    ==> F : stable (A Int B)";
 by (Blast_tac 1);
 result();
 
 

 qed "INT_le_Suc_equals_Int";
 
 
 (*The final deadlock example*)
 val [zeroprem, allprem] = goalw thy [stable_def]
-    "[| F : constrains (A 0 Int A (Suc n)) (A 0);  \
-\       ALL i: atMost n. F : constrains (A(Suc i) Int A i) \
-\                                         (-A i Un A(Suc i)) |] \
+    "[| F : (A 0 Int A (Suc n)) co (A 0);  \
+\       ALL i: atMost n. F : (A(Suc i) Int A i) co \
+\                            (-A i Un A(Suc i)) |] \
 \    ==> F : stable (INT i: atMost (Suc n). A i)";
 
 by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS 
     constrains_Int RS constrains_weaken) 1);
 by (simp_tac (simpset() addsimps [Collect_le_Int_equals,