src/ZF/Resid/Substitution.ML

 \       (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
 by (etac redexes.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by Safe_tac;
 by (case_tac "n < xa" 1);
-by ((forward_tac [lt_trans2] 1) THEN (assume_tac 1));
+by ((ftac lt_trans2 1) THEN (assume_tac 1));
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
 qed "lift_lift_rec";
 
 Goal "[|u:redexes; n:nat|] ==>  \
 \      lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))";

     THEN ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])));
 by Safe_tac;
 by (excluded_middle_tac "n < x" 1);
 by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("i","x")] leE 1);
-by (forward_tac  [lt_trans1] 1 THEN assume_tac 1);
+by (ftac lt_trans1 1 THEN assume_tac 1);
 by (ALLGOALS(asm_simp_tac 
              (simpset() addsimps [succ_pred,leI,gt_pred])));
 by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
 by (case_tac "n < xa" 1);
 by (Asm_full_simp_tac 2);

 by (excluded_middle_tac "n < x" 1);
 by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("j","n")] leE 1);
 by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
 by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1);
-by (forward_tac [lt_trans2] 1 THEN assume_tac 1);
+by (ftac lt_trans2 1 THEN assume_tac 1);
 by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
 qed "subst_rec_subst_rec";
 
 
 Goal "[|v:redexes; u:redexes; w:redexes; n:nat|] ==>  \