src/HOL/WF.ML
changeset 2031 03a843f0f447
parent 1786 8a31d85d27b8
child 2637 e9b203f854ae
     1.1 --- a/src/HOL/WF.ML	Thu Sep 26 11:11:22 1996 +0200
     1.2 +++ b/src/HOL/WF.ML	Thu Sep 26 12:47:47 1996 +0200
     1.3 @@ -129,7 +129,7 @@
     1.4    by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
     1.5                     is_the_recfun 1);
     1.6    by (rewtac is_recfun_def);
     1.7 -  by (rtac (cuts_eq RS ssubst) 1);
     1.8 +  by (stac cuts_eq 1);
     1.9    by (rtac allI 1);
    1.10    by (rtac impI 1);
    1.11    by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1);
    1.12 @@ -159,7 +159,7 @@
    1.13  by (wf_ind_tac "a" prems 1);
    1.14  by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1); 
    1.15  by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
    1.16 -by (rtac (cuts_eq RS ssubst) 1);
    1.17 +by (stac cuts_eq 1);
    1.18  (*Applying the substitution: must keep the quantified assumption!!*)
    1.19  by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac,
    1.20              etac (mp RS ssubst), atac]);