src/HOL/WF.ML
changeset 1760 6f41a494f3b1
parent 1642 21db0cf9a1a4
child 1771 ee81183a77a0
     1.1 --- a/src/HOL/WF.ML	Wed May 22 18:32:37 1996 +0200
     1.2 +++ b/src/HOL/WF.ML	Thu May 23 14:37:06 1996 +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 (HOL_cs addEs prems) 1);
     1.8 +by (fast_tac (!claset addEs 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 (HOL_cs addIs prems) 1);
    1.17 +by (fast_tac (!claset addIs prems) 1);
    1.18  by (wf_ind_tac "a" prems 1);
    1.19 -by (fast_tac set_cs 1);
    1.20 +by (Fast_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 HOL_cs 1);
    1.29 -by (fast_tac HOL_cs 1);
    1.30 +by (Fast_tac 1);
    1.31 +by (Fast_tac 1);
    1.32  qed "wf_trancl";
    1.33  
    1.34