--- a/src/HOL/UNITY/Comp/Handshake.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Comp/Handshake.thy Thu Jun 02 13:47:08 2005 +0200
@@ -49,14 +49,14 @@
apply force
apply (rule constrains_imp_Constrains [THEN StableI])
apply auto
- apply (unfold F_def, constrains)
-apply (unfold G_def, constrains)
+ apply (unfold F_def, safety)
+apply (unfold G_def, safety)
done
lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo
({s. NF s = k} Int {s. BB s})"
apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
- apply (unfold F_def, constrains)
+ apply (unfold F_def, safety)
apply (unfold G_def, ensures_tac "cmdG")
done
@@ -64,7 +64,7 @@
{s. k < NF s}"
apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
apply (unfold F_def, ensures_tac "cmdF")
-apply (unfold G_def, constrains)
+apply (unfold G_def, safety)
done
lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"