--- a/src/HOL/UNITY/Token.ML Wed Aug 05 10:56:58 1998 +0200
+++ b/src/HOL/UNITY/Token.ML Wed Aug 05 10:57:25 1998 +0200
@@ -23,7 +23,7 @@
qed "not_E_eq";
(*This proof is in the "massaging" style and is much faster! *)
-Goalw [stable_def] "stable Acts (Compl(E i) Un (HasTok i))";
+Goalw [stable_def] "stable acts (Compl(E i) Un (HasTok i))";
by (rtac constrains_weaken 1);
by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
@@ -77,7 +77,7 @@
(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
Note the use of case_tac. Reasoning about leadsTo takes practice!*)
Goal "[| i<N; j<N |] ==> \
-\ leadsTo Acts (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
+\ leadsTo acts (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
by (case_tac "i=j" 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
by (rtac (TR7 RS leadsTo_weaken_R) 1);
@@ -88,7 +88,7 @@
(*Chapter 4 variant, the one actually used below.*)
Goal "[| i<N; j<N; i~=j |] \
-\ ==> leadsTo Acts (HasTok i) {s. (token s, i) : nodeOrder j}";
+\ ==> leadsTo acts (HasTok i) {s. (token s, i) : nodeOrder j}";
by (rtac (TR7 RS leadsTo_weaken_R) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
@@ -101,7 +101,7 @@
(*Misra's TR9: the token reaches an arbitrary node*)
-Goal "j<N ==> leadsTo Acts {s. token s < N} (HasTok j)";
+Goal "j<N ==> leadsTo acts {s. token s < N} (HasTok j)";
by (rtac leadsTo_weaken_R 1);
by (res_inst_tac [("I", "Compl{j}"), ("f", "token"), ("B", "{}")]
(wf_nodeOrder RS bounded_induct) 1);
@@ -115,7 +115,7 @@
qed "leadsTo_j";
(*Misra's TR8: a hungry process eventually eats*)
-Goal "j<N ==> leadsTo Acts ({s. token s < N} Int H j) (E j)";
+Goal "j<N ==> leadsTo acts ({s. token s < N} Int H j) (E j)";
by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
by (rtac TR6 2);
by (rtac leadsTo_weaken_R 1);