src/HOL/UNITY/Token.ML

 val TR6   = forall_elim_vars 0 (thm "TR6");
 val TR7   = forall_elim_vars 0 (thm "TR7");
 val nodeOrder_def   = (thm "nodeOrder_def");
 val next_def   = (thm "next_def");
 
-AddIffs [thm "N_positive", thm"skip"];
+AddIffs [thm "N_positive"];
 
-Goalw [stable_def] "stable acts (-(E i) Un (HasTok i))";
+Goalw [stable_def] "F : stable (-(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]));
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
 qed "token_stable";

 
 
 (*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)";
+\     F : leadsTo (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);
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
 qed "TR7_nodeOrder";
 
 
 (*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}";
+\     ==> F : leadsTo (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);
 qed "TR7_aux";
 

 by Auto_tac;
 val token_lemma = result();
 
 
 (*Misra's TR9: the token reaches an arbitrary node*)
-Goal "j<N ==> leadsTo acts {s. token s < N} (HasTok j)";
+Goal "j<N ==> F : leadsTo {s. token s < N} (HasTok j)";
 by (rtac leadsTo_weaken_R 1);
 by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
      (wf_nodeOrder RS bounded_induct) 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff,
 						HasTok_def])));

 by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def])));
 by (ALLGOALS Blast_tac);
 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 ==> F : leadsTo ({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);
 by (rtac ([leadsTo_j, TR3] MRS psp) 1);
 by (ALLGOALS Blast_tac);