src/ZF/UNITY/SubstAx.ML

 qed "LeadsTo_Union";
 
 (*** Derived rules ***)
 
 Goal "F : A leadsTo B ==> F : A LeadsTo B";
-by (forward_tac [leadsToD2] 1);
+by (ftac leadsToD2 1);
 by (Clarify_tac 1);
 by (asm_simp_tac (simpset() addsimps [LeadsTo_eq]) 1);
 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
 qed "leadsTo_imp_LeadsTo";
 

 (*Lets us look at the starting state*)
 val [major, program] = Goal 
 "[|(!!s. s:A ==> F:{s} LeadsTo B); F:program|]==>F:A LeadsTo B";
 by (cut_facts_tac [program] 1);
 by (stac (UN_singleton RS sym) 1 THEN rtac LeadsTo_UN 1);
-by (forward_tac [major] 1);
+by (ftac major 1);
 by Auto_tac;
 qed "single_LeadsTo_I";
 
 Goal "[| A <= B; F:program |] ==> F : A LeadsTo B";
 by (asm_simp_tac (simpset() addsimps [LeadsTo_def]) 1);

 "[|(!!i. i:I ==> F: A(i) LeadsTo A'(i)); F:program |] \
 \     ==> F : (UN i:I. A(i)) LeadsTo (UN i:I. A'(i))";
 by (cut_facts_tac [minor] 1);
 by (rtac LeadsTo_Union 1);
 by (ALLGOALS(Clarify_tac));
-by (forward_tac [major] 1);
+by (ftac major 1);
 by (blast_tac (claset()  addIs [LeadsTo_weaken_R]) 1);
 qed "LeadsTo_UN_UN";
 
 (*Binary union version*)
 Goal "[| F:A LeadsTo A'; F:B LeadsTo B' |] ==> F:(A Un B) LeadsTo (A' Un B')";

 by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
 qed "PSP2";
 
 Goal
 "[| F : A LeadsTo A'; F : B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')";
-by (rewrite_goals_tac [Unless_def]);
+by (rewtac Unless_def);
 by (dtac PSP 1);
 by (assume_tac 1);
 by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, subset_imp_LeadsTo]) 1);
 qed "PSP_Unless";