src/HOL/UNITY/Token.ML
changeset 7403 c318acb88251
parent 6711 d45359e7dcbf
child 8395 919307bebbef
     1.1 --- a/src/HOL/UNITY/Token.ML	Wed Sep 01 11:15:35 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Token.ML	Wed Sep 01 11:16:02 1999 +0200
     1.3 @@ -71,8 +71,7 @@
     1.4  by (case_tac "i=j" 1);
     1.5  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
     1.6  by (rtac (TR7 RS leadsTo_weaken_R) 1);
     1.7 -by (Clarify_tac 1);
     1.8 -by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
     1.9 +by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
    1.10  qed "TR7_nodeOrder";
    1.11  
    1.12  
    1.13 @@ -80,8 +79,7 @@
    1.14  Goal "[| i<N; j<N; i~=j |]    \
    1.15  \     ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}";
    1.16  by (rtac (TR7 RS leadsTo_weaken_R) 1);
    1.17 -by (Clarify_tac 1);
    1.18 -by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
    1.19 +by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
    1.20  qed "TR7_aux";
    1.21  
    1.22  Goal "({s. token s < N} Int token -`` {m}) = \
    1.23 @@ -100,15 +98,13 @@
    1.24  by (Blast_tac 2);
    1.25  by (Clarify_tac 1);
    1.26  by (rtac (TR7_aux RS leadsTo_weaken) 1);
    1.27 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def])));
    1.28 -by (ALLGOALS Blast_tac);
    1.29 +by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_def]));
    1.30  qed "leadsTo_j";
    1.31  
    1.32  (*Misra's TR8: a hungry process eventually eats*)
    1.33  Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)";
    1.34  by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
    1.35  by (rtac TR6 2);
    1.36 -by (rtac leadsTo_weaken 1);
    1.37 -by (rtac ([leadsTo_j, TR3] MRS psp) 1);
    1.38 +by (rtac ([leadsTo_j, TR3] MRS psp RS leadsTo_weaken) 1);
    1.39  by (ALLGOALS Blast_tac);
    1.40  qed "token_progress";