--- a/src/HOL/UNITY/Deadlock.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Deadlock.ML Thu Apr 29 10:51:58 1999 +0200
@@ -9,7 +9,7 @@
(*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();
@@ -69,9 +69,9 @@
(*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