src/HOL/WF.ML
changeset 2935 998cb95fdd43
parent 2637 e9b203f854ae
child 3198 295287618e30
     1.1 --- a/src/HOL/WF.ML	Fri Apr 11 11:33:51 1997 +0200
     1.2 +++ b/src/HOL/WF.ML	Fri Apr 11 15:21:36 1997 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  \       !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
     1.5  \    |]  ==>  P(a)";
     1.6  by (rtac (major RS spec RS mp RS spec) 1);
     1.7 -by (fast_tac (!claset addEs prems) 1);
     1.8 +by (blast_tac (!claset addIs prems) 1);
     1.9  qed "wf_induct";
    1.10  
    1.11  (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
    1.12 @@ -38,9 +38,9 @@
    1.13  
    1.14  val prems = goal WF.thy "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
    1.15  by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
    1.16 -by (fast_tac (!claset addIs prems) 1);
    1.17 +by (blast_tac (!claset addIs prems) 1);
    1.18  by (wf_ind_tac "a" prems 1);
    1.19 -by (Fast_tac 1);
    1.20 +by (Blast_tac 1);
    1.21  qed "wf_asym";
    1.22  
    1.23  val prems = goal WF.thy "[| wf(r);  (a,a): r |] ==> P";
    1.24 @@ -58,8 +58,8 @@
    1.25  by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
    1.26  by (rtac (impI RS allI) 1);
    1.27  by (etac tranclE 1);
    1.28 -by (Fast_tac 1);
    1.29 -by (Fast_tac 1);
    1.30 +by (Blast_tac 1);
    1.31 +by (Blast_tac 1);
    1.32  qed "wf_trancl";
    1.33  
    1.34