isatool expandshort;
authorwenzelm
Tue Sep 07 10:40:58 1999 +0200 (1999-09-07)
changeset 749923e090051cb8
parent 7498 1e5585fd3632
child 7500 299949eddba8
isatool expandshort;
src/HOL/Auth/KerberosIV.ML
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom_Bad.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/Hoare/Arith2.ML
src/HOL/IOA/IOA.ML
src/HOL/IOA/Solve.ML
src/HOL/Induct/LFilter.ML
src/HOL/Induct/Multiset.ML
src/HOL/Induct/Mutil.ML
src/HOL/Integ/IntDiv.ML
src/HOL/MiniML/Instance.ML
src/HOL/MiniML/W.ML
src/HOL/Real/Hyperreal/Filter.ML
src/HOL/Real/Hyperreal/HyperDef.ML
src/HOL/Real/Hyperreal/Zorn.ML
src/HOL/Real/PReal.ML
src/HOL/Real/RComplete.ML
src/HOL/Real/RealDef.ML
src/HOL/Real/RealOrd.ML
src/HOL/Set.ML
src/HOL/Subst/UTerm.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/UNITY/Channel.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/GenPrefix.ML
src/HOL/UNITY/Lift_prog.ML
src/HOL/W0/I.ML
src/HOL/W0/W.ML
src/HOL/WF.ML
src/HOL/ex/MT.ML
src/HOL/ex/Tarski.ML
src/HOLCF/Cont.ML
src/HOLCF/IOA/NTP/Correctness.ML
src/HOLCF/IOA/meta_theory/Abstraction.ML
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/Deadlock.ML
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/Sprod2.ML
src/ZF/AC/AC15_WO6.ML
src/ZF/AC/AC16_WO4.ML
src/ZF/AC/AC16_lemmas.ML
src/ZF/AC/AC2_AC6.ML
src/ZF/AC/AC_Equiv.ML
src/ZF/AC/DC.ML
src/ZF/AC/DC_lemmas.ML
src/ZF/AC/HH.ML
src/ZF/AC/WO1_WO7.ML
src/ZF/AC/WO2_AC16.ML
src/ZF/AC/WO6_WO1.ML
src/ZF/Arith.ML
src/ZF/Cardinal.ML
src/ZF/CardinalArith.ML
src/ZF/Coind/MT.ML
src/ZF/Coind/Map.ML
src/ZF/IMP/Equiv.ML
src/ZF/Order.ML
src/ZF/OrderType.ML
src/ZF/Resid/Confluence.ML
src/ZF/Resid/Substitution.ML
src/ZF/Zorn.ML
src/ZF/ex/Primrec.ML
src/ZF/ex/Term.ML
src/ZF/func.ML
     1.1 --- a/src/HOL/Auth/KerberosIV.ML	Mon Sep 06 22:12:08 1999 +0200
     1.2 +++ b/src/HOL/Auth/KerberosIV.ML	Tue Sep 07 10:40:58 1999 +0200
     1.3 @@ -148,10 +148,10 @@
     1.4  fun parts_induct_tac i = 
     1.5      etac kerberos.induct i  THEN 
     1.6      REPEAT (FIRSTGOAL analz_mono_contra_tac)  THEN
     1.7 -    forward_tac [K3_msg_in_parts_spies] (i+4)  THEN
     1.8 -    forward_tac [K5_msg_in_parts_spies] (i+6)  THEN
     1.9 -    forward_tac [Oops_parts_spies1] (i+8)  THEN
    1.10 -    forward_tac [Oops_parts_spies2] (i+9) THEN
    1.11 +    ftac K3_msg_in_parts_spies (i+4)  THEN
    1.12 +    ftac K5_msg_in_parts_spies (i+6)  THEN
    1.13 +    ftac Oops_parts_spies1 (i+8)  THEN
    1.14 +    ftac Oops_parts_spies2 (i+9) THEN
    1.15      prove_simple_subgoals_tac 1;
    1.16  
    1.17  
    1.18 @@ -247,7 +247,7 @@
    1.19  \          : parts (spies evs);\
    1.20  \        evs : kerberos |]    \
    1.21  \     ==> AuthKey : AuthKeys evs";
    1.22 -by (forward_tac [A_trusts_AuthTicket] 1);
    1.23 +by (ftac A_trusts_AuthTicket 1);
    1.24  by (assume_tac 1);
    1.25  by (simp_tac (simpset() addsimps [AuthKeys_def]) 1);
    1.26  by (Blast_tac 1);
    1.27 @@ -497,7 +497,7 @@
    1.28   "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \
    1.29  \             : set evs;    \
    1.30  \           evs : kerberos |] ==> KeyCryptKey AuthKey ServKey evs";
    1.31 -by (forward_tac [Says_Tgs_message_form] 1);
    1.32 +by (ftac Says_Tgs_message_form 1);
    1.33  by (assume_tac 1);
    1.34  by (Blast_tac 1);
    1.35  qed "KeyCryptKeyI";
    1.36 @@ -643,10 +643,10 @@
    1.37  val analz_sees_tac = 
    1.38    EVERY 
    1.39     [REPEAT (FIRSTGOAL analz_mono_contra_tac),
    1.40 -    forward_tac [Oops_range_spies2] 10, 
    1.41 -    forward_tac [Oops_range_spies1] 9, 
    1.42 -    forward_tac [Says_tgs_message_form] 7,
    1.43 -    forward_tac [Says_kas_message_form] 5, 
    1.44 +    ftac Oops_range_spies2 10, 
    1.45 +    ftac Oops_range_spies1 9, 
    1.46 +    ftac Says_tgs_message_form 7,
    1.47 +    ftac Says_kas_message_form 5, 
    1.48      REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE]
    1.49  		  ORELSE' hyp_subst_tac)];
    1.50  
    1.51 @@ -700,14 +700,14 @@
    1.52  (*Oops 2*)
    1.53  by (case_tac "Key ServKey : analz (spies evsO2)" 2);
    1.54  by (ALLGOALS Asm_full_simp_tac);
    1.55 -by (forward_tac [analz_mono_KK] 2
    1.56 +by (ftac analz_mono_KK 2
    1.57      THEN assume_tac 2
    1.58      THEN assume_tac 2);
    1.59 -by (forward_tac [analz_cut] 2 THEN assume_tac 2);
    1.60 +by (ftac analz_cut 2 THEN assume_tac 2);
    1.61  by (blast_tac (claset() addDs [analz_cut, impOfSubs analz_mono]) 2);
    1.62  by (dres_inst_tac [("x","SK")] spec 2);
    1.63  by (dres_inst_tac [("x","insert ServKey KK")] spec 2);
    1.64 -by (forward_tac [Says_Tgs_message_form] 2 THEN assume_tac 2);
    1.65 +by (ftac Says_Tgs_message_form 2 THEN assume_tac 2);
    1.66  by (Clarify_tac 2);
    1.67  by (forward_tac [Says_imp_spies RS parts.Inj RS parts.Body 
    1.68                   RS parts.Snd RS parts.Snd RS parts.Snd] 2);
    1.69 @@ -732,7 +732,7 @@
    1.70  \        SesKey ~: range shrK |]                                 \
    1.71  \     ==> Key K : analz (insert (Key SesKey) (spies evs)) = \
    1.72  \         (K = SesKey | Key K : analz (spies evs))";
    1.73 -by (forward_tac [AuthKeys_are_not_KeyCryptKey] 1 THEN assume_tac 1);
    1.74 +by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1);
    1.75  by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
    1.76  qed "analz_insert_freshK1";
    1.77  
    1.78 @@ -742,7 +742,7 @@
    1.79  Goal "[| evs : kerberos;  ServKey ~: (AuthKeys evs); ServKey ~: range shrK|]\
    1.80  \     ==> Key K : analz (insert (Key ServKey) (spies evs)) = \
    1.81  \         (K = ServKey | Key K : analz (spies evs))";
    1.82 -by (forward_tac [not_AuthKeys_not_KeyCryptKey] 1 
    1.83 +by (ftac not_AuthKeys_not_KeyCryptKey 1 
    1.84      THEN assume_tac 1
    1.85      THEN assume_tac 1);
    1.86  by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
    1.87 @@ -837,7 +837,7 @@
    1.88  \        ~ ExpirAuth Tk evs;                         \
    1.89  \        A ~: bad;  evs : kerberos |]            \
    1.90  \     ==> Key AuthKey ~: analz (spies evs)";
    1.91 -by (forward_tac [Says_Kas_message_form] 1 THEN assume_tac 1);
    1.92 +by (ftac Says_Kas_message_form 1 THEN assume_tac 1);
    1.93  by (blast_tac (claset() addSDs [lemma]) 1);
    1.94  qed "Confidentiality_Kas";
    1.95  
    1.96 @@ -890,7 +890,7 @@
    1.97                                 Key_unique_SesKey] addIs [less_SucI]) 3);
    1.98  (** Level 12 **)
    1.99  (*Oops1*)
   1.100 -by (forward_tac [Says_Kas_message_form] 2);
   1.101 +by (ftac Says_Kas_message_form 2);
   1.102  by (assume_tac 2);
   1.103  by (blast_tac (claset() addDs [analz_insert_freshK3,
   1.104  			       Says_Kas_message_form, Says_Tgs_message_form] 
   1.105 @@ -917,7 +917,7 @@
   1.106  \           ~ ExpirServ Tt evs;                         \
   1.107  \           A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
   1.108  \        ==> Key ServKey ~: analz (spies evs)";
   1.109 -by (forward_tac [Says_Tgs_message_form] 1 THEN assume_tac 1);
   1.110 +by (ftac Says_Tgs_message_form 1 THEN assume_tac 1);
   1.111  by (blast_tac (claset() addDs [lemma]) 1);
   1.112  qed "Confidentiality_Tgs1";
   1.113  
   1.114 @@ -953,7 +953,7 @@
   1.115  \    evs : kerberos |]         \
   1.116  \==> Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\
   1.117  \      : set evs";
   1.118 -by (forward_tac [Says_Kas_message_form] 1 THEN assume_tac 1);
   1.119 +by (ftac Says_Kas_message_form 1 THEN assume_tac 1);
   1.120  by (etac rev_mp 1);
   1.121  by (etac rev_mp 1);
   1.122  by (etac rev_mp 1);
   1.123 @@ -1055,9 +1055,9 @@
   1.124  \    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
   1.125  \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
   1.126  \      : set evs";
   1.127 -by (forward_tac [B_trusts_ServKey] 1);
   1.128 +by (ftac B_trusts_ServKey 1);
   1.129  by (etac exE 4);
   1.130 -by (forward_tac [K4_imp_K2] 4);
   1.131 +by (ftac K4_imp_K2 4);
   1.132  by (Blast_tac 5);
   1.133  by (ALLGOALS assume_tac);
   1.134  qed "B_trusts_ServTicket";
   1.135 @@ -1073,9 +1073,9 @@
   1.136  \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
   1.137  \      : set evs         \
   1.138  \    & ServLife + Tt <= AuthLife + Tk)";
   1.139 -by (forward_tac [B_trusts_ServKey] 1);
   1.140 +by (ftac B_trusts_ServKey 1);
   1.141  by (etac exE 4);
   1.142 -by (forward_tac [K4_imp_K2_refined] 4);
   1.143 +by (ftac K4_imp_K2_refined 4);
   1.144  by (Blast_tac 5);
   1.145  by (ALLGOALS assume_tac);
   1.146  qed "B_trusts_ServTicket_refined";
   1.147 @@ -1096,12 +1096,12 @@
   1.148  \        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;     \
   1.149  \        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
   1.150  \     ==> Key ServKey ~: analz (spies evs)";
   1.151 -by (forward_tac [A_trusts_AuthKey] 1);
   1.152 -by (forward_tac [Confidentiality_Kas] 3);
   1.153 -by (forward_tac [B_trusts_ServTicket] 6);
   1.154 +by (ftac A_trusts_AuthKey 1);
   1.155 +by (ftac Confidentiality_Kas 3);
   1.156 +by (ftac B_trusts_ServTicket 6);
   1.157  by (etac exE 9);
   1.158  by (etac exE 9);
   1.159 -by (forward_tac [Says_Kas_message_form] 9);
   1.160 +by (ftac Says_Kas_message_form 9);
   1.161  by (blast_tac (claset() addDs [A_trusts_K4, 
   1.162                                 unique_ServKeys, unique_AuthKeys,
   1.163                                 Confidentiality_Tgs2]) 10);
   1.164 @@ -1143,7 +1143,7 @@
   1.165  \        ~ ExpirAuth Tk evs; A ~: bad; evs : kerberos |]         \
   1.166  \==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
   1.167  \      : set evs";
   1.168 -by (forward_tac [A_trusts_AuthKey] 1 THEN assume_tac 1 THEN assume_tac 1);
   1.169 +by (ftac A_trusts_AuthKey 1 THEN assume_tac 1 THEN assume_tac 1);
   1.170  by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1);
   1.171  qed "A_trusts_ServKey"; 
   1.172  (*Note: requires a temporal check*)
   1.173 @@ -1170,8 +1170,8 @@
   1.174  by (etac rev_mp 1);
   1.175  by (etac rev_mp 1);
   1.176  by (etac kerberos.induct 1);
   1.177 -by (forward_tac [Says_ticket_in_parts_spies] 5);
   1.178 -by (forward_tac [Says_ticket_in_parts_spies] 7);
   1.179 +by (ftac Says_ticket_in_parts_spies 5);
   1.180 +by (ftac Says_ticket_in_parts_spies 7);
   1.181  by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
   1.182  by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.183  by (Fake_parts_insert_tac 1);
   1.184 @@ -1198,8 +1198,8 @@
   1.185  \        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
   1.186  \  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
   1.187  \                 Crypt ServKey {|Agent A, Number Ta|} |} : set evs";
   1.188 -by (forward_tac [Confidentiality_B] 1);
   1.189 -by (forward_tac [B_trusts_ServKey] 9);
   1.190 +by (ftac Confidentiality_B 1);
   1.191 +by (ftac B_trusts_ServKey 9);
   1.192  by (etac exE 12);
   1.193  by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
   1.194                          addSIs [Says_Auth]) 12);
   1.195 @@ -1214,8 +1214,8 @@
   1.196  \        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
   1.197  \  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
   1.198  \                 Crypt ServKey {|Agent A, Number Ta2|} |} : set evs";
   1.199 -by (forward_tac [Confidentiality_B_refined] 1);
   1.200 -by (forward_tac [B_trusts_ServKey] 6);
   1.201 +by (ftac Confidentiality_B_refined 1);
   1.202 +by (ftac B_trusts_ServKey 6);
   1.203  by (etac exE 9);
   1.204  by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
   1.205                          addSIs [Says_Auth]) 9);
   1.206 @@ -1235,14 +1235,14 @@
   1.207  by (etac rev_mp 1);
   1.208  by (etac rev_mp 1);
   1.209  by (etac kerberos.induct 1);
   1.210 -by (forward_tac [Says_ticket_in_parts_spies] 5);
   1.211 -by (forward_tac [Says_ticket_in_parts_spies] 7);
   1.212 +by (ftac Says_ticket_in_parts_spies 5);
   1.213 +by (ftac Says_ticket_in_parts_spies 7);
   1.214  by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
   1.215  by (ALLGOALS Asm_simp_tac);
   1.216  by (Fake_parts_insert_tac 1);
   1.217  by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
   1.218  by (Clarify_tac 1);
   1.219 -by (forward_tac [Says_Tgs_message_form] 1 THEN assume_tac 1);
   1.220 +by (ftac Says_Tgs_message_form 1 THEN assume_tac 1);
   1.221  by (Clarify_tac 1);  (*PROOF FAILED if omitted*)
   1.222  by (blast_tac (claset() addDs [unique_CryptKey] addEs spies_partsEs) 1);
   1.223  qed "Says_K6";
   1.224 @@ -1269,13 +1269,13 @@
   1.225  \        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
   1.226  \        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
   1.227  \     ==> Says B A (Crypt ServKey (Number Ta)) : set evs";
   1.228 -by (forward_tac [A_trusts_AuthKey] 1);
   1.229 -by (forward_tac [Says_Kas_message_form] 3);
   1.230 -by (forward_tac [Confidentiality_Kas] 4);
   1.231 -by (forward_tac [K4_trustworthy] 7);
   1.232 +by (ftac A_trusts_AuthKey 1);
   1.233 +by (ftac Says_Kas_message_form 3);
   1.234 +by (ftac Confidentiality_Kas 4);
   1.235 +by (ftac K4_trustworthy 7);
   1.236  by (Blast_tac 8);
   1.237  by (etac exE 9);
   1.238 -by (forward_tac [K4_imp_K2] 9);
   1.239 +by (ftac K4_imp_K2 9);
   1.240  by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
   1.241                          addSIs [Says_K6]
   1.242                          addSEs [Confidentiality_Tgs1 RSN (2,rev_notE)]) 10);
   1.243 @@ -1298,8 +1298,8 @@
   1.244  by (etac rev_mp 1);
   1.245  by (etac rev_mp 1);
   1.246  by (etac kerberos.induct 1);
   1.247 -by (forward_tac [Says_ticket_in_parts_spies] 5);
   1.248 -by (forward_tac [Says_ticket_in_parts_spies] 7);
   1.249 +by (ftac Says_ticket_in_parts_spies 5);
   1.250 +by (ftac Says_ticket_in_parts_spies 7);
   1.251  by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
   1.252  by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.253  by (Fake_parts_insert_tac 1);
   1.254 @@ -1399,8 +1399,8 @@
   1.255  by (etac rev_mp 1);
   1.256  by (etac rev_mp 1);
   1.257  by (etac kerberos.induct 1);
   1.258 -by (forward_tac [Says_ticket_in_parts_spies] 5);
   1.259 -by (forward_tac [Says_ticket_in_parts_spies] 7);
   1.260 +by (ftac Says_ticket_in_parts_spies 5);
   1.261 +by (ftac Says_ticket_in_parts_spies 7);
   1.262  by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
   1.263  by (ALLGOALS Asm_simp_tac);
   1.264  by (Clarify_tac 1);
     2.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Mon Sep 06 22:12:08 1999 +0200
     2.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Tue Sep 07 10:40:58 1999 +0200
     2.3 @@ -53,8 +53,8 @@
     2.4  (*For proving the easier theorems about X ~: parts (spies evs).*)
     2.5  fun parts_induct_tac i = 
     2.6      etac kerberos_ban.induct i  THEN 
     2.7 -    forward_tac [Oops_parts_spies] (i+6)  THEN
     2.8 -    forward_tac [Kb3_msg_in_parts_spies] (i+4)     THEN
     2.9 +    ftac Oops_parts_spies (i+6)  THEN
    2.10 +    ftac Kb3_msg_in_parts_spies (i+4)     THEN
    2.11      prove_simple_subgoals_tac i;
    2.12  
    2.13  
    2.14 @@ -160,8 +160,8 @@
    2.15  
    2.16  (*For proofs involving analz.*)
    2.17  val analz_spies_tac = 
    2.18 -    forward_tac [Says_Server_message_form] 7 THEN
    2.19 -    forward_tac [Says_S_message_form] 5 THEN 
    2.20 +    ftac Says_Server_message_form 7 THEN
    2.21 +    ftac Says_S_message_form 5 THEN 
    2.22      REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
    2.23  
    2.24  
    2.25 @@ -266,7 +266,7 @@
    2.26  \        ~ Expired T evs;                                        \
    2.27  \        A ~: bad;  B ~: bad;  evs : kerberos_ban                \
    2.28  \     |] ==> Key K ~: analz (spies evs)";
    2.29 -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    2.30 +by (ftac Says_Server_message_form 1 THEN assume_tac 1);
    2.31  by (blast_tac (claset() addIs [lemma2]) 1);
    2.32  qed "Confidentiality_S";
    2.33  
    2.34 @@ -304,9 +304,9 @@
    2.35  \         Crypt K (Number Ta) : parts (spies evs) -->        \
    2.36  \         Says B A (Crypt K (Number Ta)) : set evs";
    2.37  by (etac kerberos_ban.induct 1);
    2.38 -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
    2.39 +by (ftac Says_S_message_form 5 THEN assume_tac 5);     
    2.40  by (dtac Kb3_msg_in_parts_spies 5);
    2.41 -by (forward_tac [Oops_parts_spies] 7);
    2.42 +by (ftac Oops_parts_spies 7);
    2.43  by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
    2.44  by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
    2.45  (**LEVEL 6**)
    2.46 @@ -349,9 +349,9 @@
    2.47  \        Says A B {|X, Crypt K {|Agent A, Number Ta|}|}  \
    2.48  \            : set evs";
    2.49  by (etac kerberos_ban.induct 1);
    2.50 -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
    2.51 -by (forward_tac [Kb3_msg_in_parts_spies] 5);
    2.52 -by (forward_tac [Oops_parts_spies] 7);
    2.53 +by (ftac Says_S_message_form 5 THEN assume_tac 5);     
    2.54 +by (ftac Kb3_msg_in_parts_spies 5);
    2.55 +by (ftac Oops_parts_spies 7);
    2.56  by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
    2.57  by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
    2.58  (**LEVEL 6**)
     3.1 --- a/src/HOL/Auth/NS_Shared.ML	Mon Sep 06 22:12:08 1999 +0200
     3.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Sep 07 10:40:58 1999 +0200
     3.3 @@ -50,8 +50,8 @@
     3.4  fun parts_induct_tac i = 
     3.5    EVERY [etac ns_shared.induct i,
     3.6  	 REPEAT (FIRSTGOAL analz_mono_contra_tac),
     3.7 -	 forward_tac [Oops_parts_spies] (i+7),
     3.8 -	 forward_tac [NS3_msg_in_parts_spies] (i+4),
     3.9 +	 ftac Oops_parts_spies (i+7),
    3.10 +	 ftac NS3_msg_in_parts_spies (i+4),
    3.11  	 prove_simple_subgoals_tac i];
    3.12  
    3.13  
    3.14 @@ -140,8 +140,8 @@
    3.15  
    3.16  (*For proofs involving analz.*)
    3.17  val analz_spies_tac = 
    3.18 -    forward_tac [Says_Server_message_form] 8 THEN
    3.19 -    forward_tac [Says_S_message_form] 5 THEN 
    3.20 +    ftac Says_Server_message_form 8 THEN
    3.21 +    ftac Says_S_message_form 5 THEN 
    3.22      REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
    3.23  
    3.24  
    3.25 @@ -263,7 +263,7 @@
    3.26  \           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;      \
    3.27  \           A ~: bad;  B ~: bad;  evs : ns_shared                \
    3.28  \        |] ==> Key K ~: analz (spies evs)";
    3.29 -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    3.30 +by (ftac Says_Server_message_form 1 THEN assume_tac 1);
    3.31  by (blast_tac (claset() delrules [notI]
    3.32  			addIs [lemma2]) 1);
    3.33  qed "Spy_not_see_encrypted_key";
     4.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Sep 06 22:12:08 1999 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Sep 07 10:40:58 1999 +0200
     4.3 @@ -70,9 +70,9 @@
     4.4  (*For proving the easier theorems about X ~: parts (knows Spy evs).*)
     4.5  fun parts_induct_tac i = 
     4.6      etac otway.induct i			THEN 
     4.7 -    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
     4.8 -    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
     4.9 -    forward_tac [OR2_parts_knows_Spy]  (i+4) THEN 
    4.10 +    ftac Oops_parts_knows_Spy (i+7) THEN
    4.11 +    ftac OR4_parts_knows_Spy (i+6) THEN
    4.12 +    ftac OR2_parts_knows_Spy (i+4) THEN 
    4.13      prove_simple_subgoals_tac  i;
    4.14  
    4.15  
    4.16 @@ -130,7 +130,7 @@
    4.17  val analz_knows_Spy_tac = 
    4.18      dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN 
    4.19      dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
    4.20 -    forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
    4.21 +    ftac Says_Server_message_form 8 THEN assume_tac 8 THEN
    4.22      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
    4.23  
    4.24  
    4.25 @@ -327,7 +327,7 @@
    4.26  \        Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
    4.27  \        A ~: bad;  B ~: bad;  evs : otway |]                    \
    4.28  \     ==> Key K ~: analz (knows Spy evs)";
    4.29 -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    4.30 +by (ftac Says_Server_message_form 1 THEN assume_tac 1);
    4.31  by (blast_tac (claset() addSEs [lemma]) 1);
    4.32  qed "Spy_not_see_encrypted_key";
    4.33  
     5.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Sep 06 22:12:08 1999 +0200
     5.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 07 10:40:58 1999 +0200
     5.3 @@ -63,8 +63,8 @@
     5.4  (*For proving the easier theorems about X ~: parts (knows Spy evs).*)
     5.5  fun parts_induct_tac i = 
     5.6      etac otway.induct i			THEN 
     5.7 -    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
     5.8 -    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
     5.9 +    ftac Oops_parts_knows_Spy (i+7) THEN
    5.10 +    ftac OR4_parts_knows_Spy (i+6) THEN
    5.11      prove_simple_subgoals_tac  i;
    5.12  
    5.13  
    5.14 @@ -123,7 +123,7 @@
    5.15  (*For proofs involving analz.*)
    5.16  val analz_knows_Spy_tac = 
    5.17      dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
    5.18 -    forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
    5.19 +    ftac Says_Server_message_form 8 THEN assume_tac 8 THEN
    5.20      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
    5.21  
    5.22  
    5.23 @@ -261,7 +261,7 @@
    5.24  \        Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
    5.25  \        A ~: bad;  B ~: bad;  evs : otway |]                    \
    5.26  \     ==> Key K ~: analz (knows Spy evs)";
    5.27 -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    5.28 +by (ftac Says_Server_message_form 1 THEN assume_tac 1);
    5.29  by (blast_tac (claset() addSEs [lemma]) 1);
    5.30  qed "Spy_not_see_encrypted_key";
    5.31  
     6.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon Sep 06 22:12:08 1999 +0200
     6.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 07 10:40:58 1999 +0200
     6.3 @@ -74,9 +74,9 @@
     6.4  (*For proving the easier theorems about X ~: parts (knows Spy evs).*)
     6.5  fun parts_induct_tac i = 
     6.6      etac otway.induct i			THEN 
     6.7 -    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
     6.8 -    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
     6.9 -    forward_tac [OR2_parts_knows_Spy]  (i+4) THEN 
    6.10 +    ftac Oops_parts_knows_Spy (i+7) THEN
    6.11 +    ftac OR4_parts_knows_Spy (i+6) THEN
    6.12 +    ftac OR2_parts_knows_Spy (i+4) THEN 
    6.13      prove_simple_subgoals_tac  i;
    6.14  
    6.15  
    6.16 @@ -134,7 +134,7 @@
    6.17  val analz_knows_Spy_tac = 
    6.18      dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN 
    6.19      dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
    6.20 -    forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
    6.21 +    ftac Says_Server_message_form 8 THEN assume_tac 8 THEN
    6.22      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
    6.23  
    6.24  
    6.25 @@ -229,7 +229,7 @@
    6.26  \        Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
    6.27  \        A ~: bad;  B ~: bad;  evs : otway |]                    \
    6.28  \     ==> Key K ~: analz (knows Spy evs)";
    6.29 -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    6.30 +by (ftac Says_Server_message_form 1 THEN assume_tac 1);
    6.31  by (blast_tac (claset() addSEs [lemma]) 1);
    6.32  qed "Spy_not_see_encrypted_key";
    6.33  
     7.1 --- a/src/HOL/Auth/Recur.ML	Mon Sep 06 22:12:08 1999 +0200
     7.2 +++ b/src/HOL/Auth/Recur.ML	Tue Sep 07 10:40:58 1999 +0200
     7.3 @@ -112,9 +112,9 @@
     7.4  (*For proving the easier theorems about X ~: parts (spies evs).*)
     7.5  fun parts_induct_tac i = 
     7.6    EVERY [etac recur.induct i,
     7.7 -	 forward_tac [RA4_parts_spies] (i+5),
     7.8 -	 forward_tac [respond_imp_responses] (i+4),
     7.9 -	 forward_tac [RA2_parts_spies] (i+3),
    7.10 +	 ftac RA4_parts_spies (i+5),
    7.11 +	 ftac respond_imp_responses (i+4),
    7.12 +	 ftac RA2_parts_spies (i+3),
    7.13  	 prove_simple_subgoals_tac i];
    7.14  
    7.15  
    7.16 @@ -175,7 +175,7 @@
    7.17  (*For proofs involving analz.*)
    7.18  val analz_spies_tac = 
    7.19      dtac RA2_analz_spies 4 THEN 
    7.20 -    forward_tac [respond_imp_responses] 5                THEN
    7.21 +    ftac respond_imp_responses 5                THEN
    7.22      dtac RA4_analz_spies 6;
    7.23  
    7.24  
    7.25 @@ -354,8 +354,8 @@
    7.26  \         Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
    7.27  \         Key K ~: analz (insert RB (spies evs))";
    7.28  by (etac respond.induct 1);
    7.29 -by (forward_tac [respond_imp_responses] 2);
    7.30 -by (forward_tac [respond_imp_not_used] 2);
    7.31 +by (ftac respond_imp_responses 2);
    7.32 +by (ftac respond_imp_not_used 2);
    7.33  by (ALLGOALS (*6 seconds*)
    7.34      (asm_simp_tac 
    7.35       (analz_image_freshK_ss 
     8.1 --- a/src/HOL/Auth/WooLam.ML	Mon Sep 06 22:12:08 1999 +0200
     8.2 +++ b/src/HOL/Auth/WooLam.ML	Tue Sep 07 10:40:58 1999 +0200
     8.3 @@ -39,7 +39,7 @@
     8.4  (*For proving the easier theorems about X ~: parts (spies evs) *)
     8.5  fun parts_induct_tac i = 
     8.6      etac woolam.induct i  THEN 
     8.7 -    forward_tac [WL4_parts_spies] (i+5)  THEN
     8.8 +    ftac WL4_parts_spies (i+5)  THEN
     8.9      prove_simple_subgoals_tac 1;
    8.10  
    8.11  
     9.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Sep 06 22:12:08 1999 +0200
     9.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Sep 07 10:40:58 1999 +0200
     9.3 @@ -38,7 +38,7 @@
     9.4  AddDs [Gets_imp_knows_Spy RS parts.Inj];
     9.5  
     9.6  fun g_not_bad_tac s = 
     9.7 -  forward_tac [Gets_imp_Says] THEN' assume_tac THEN' not_bad_tac s;
     9.8 +  ftac Gets_imp_Says THEN' assume_tac THEN' not_bad_tac s;
     9.9  
    9.10  
    9.11  (**** Inductive proofs about yahalom ****)
    9.12 @@ -65,8 +65,8 @@
    9.13  (*For proving the easier theorems about X ~: parts (knows Spy evs).*)
    9.14  fun parts_knows_Spy_tac i = 
    9.15    EVERY
    9.16 -   [forward_tac [YM4_Key_parts_knows_Spy] (i+7),
    9.17 -    forward_tac [YM4_parts_knows_Spy] (i+6), assume_tac (i+6),
    9.18 +   [ftac YM4_Key_parts_knows_Spy (i+7),
    9.19 +    ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6),
    9.20      prove_simple_subgoals_tac i];
    9.21  
    9.22  (*Induction for regularity theorems.  If induction formula has the form
    9.23 @@ -132,7 +132,7 @@
    9.24  
    9.25  (*For proofs involving analz.*)
    9.26  val analz_knows_Spy_tac = 
    9.27 -    forward_tac [YM4_analz_knows_Spy] 7 THEN assume_tac 7;
    9.28 +    ftac YM4_analz_knows_Spy 7 THEN assume_tac 7;
    9.29  
    9.30  (****
    9.31   The following is to prove theorems of the form
    9.32 @@ -512,7 +512,7 @@
    9.33  by (g_not_bad_tac "Aa" 1);
    9.34  by (dtac (Gets_imp_knows_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
    9.35      THEN assume_tac 1);
    9.36 -by (forward_tac [Says_Server_imp_YM2] 3);
    9.37 +by (ftac Says_Server_imp_YM2 3);
    9.38  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
    9.39  (*  use Says_unique_NB to identify message components: Aa=A, Ba=B*)
    9.40  by (blast_tac (claset() addDs [Says_unique_NB, 
    9.41 @@ -520,7 +520,7 @@
    9.42  (** LEVEL 13 **)
    9.43  (*Oops case: if the nonce is betrayed now, show that the Oops event is 
    9.44    covered by the quantified Oops assumption.*)
    9.45 -by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
    9.46 +by (ftac Says_Server_imp_YM2 1 THEN assume_tac 1);
    9.47  by (expand_case_tac "NB = NBa" 1);
    9.48  (*If NB=NBa then all other components of the Oops message agree*)
    9.49  by (blast_tac (claset() addDs [Says_unique_NB]) 1);
    9.50 @@ -550,12 +550,12 @@
    9.51  \                            Nonce NA, Nonce NB|},                       \
    9.52  \                    Crypt (shrK B) {|Agent A, Key K|}|}                 \
    9.53  \            : set evs";
    9.54 -by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
    9.55 +by (ftac Spy_not_see_NB 1 THEN REPEAT (assume_tac 1));
    9.56  by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN
    9.57      assume_tac 1 THEN dtac B_trusts_YM4_shrK 1);
    9.58  by (dtac B_trusts_YM4_newK 3);
    9.59  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
    9.60 -by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
    9.61 +by (ftac Says_Server_imp_YM2 1 THEN assume_tac 1);
    9.62  by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
    9.63  by (blast_tac (claset() addDs [Says_unique_NB]) 1);
    9.64  qed "B_trusts_YM4";
    9.65 @@ -650,7 +650,7 @@
    9.66  \        (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs);     \
    9.67  \        A ~: bad;  B ~: bad;  evs : yahalom |]       \
    9.68  \     ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    9.69 -by (forward_tac [B_trusts_YM4] 1);
    9.70 +by (ftac B_trusts_YM4 1);
    9.71  by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
    9.72  by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1);
    9.73  by (rtac A_Said_YM3_lemma 1);
    10.1 --- a/src/HOL/Auth/Yahalom2.ML	Mon Sep 06 22:12:08 1999 +0200
    10.2 +++ b/src/HOL/Auth/Yahalom2.ML	Tue Sep 07 10:40:58 1999 +0200
    10.3 @@ -64,8 +64,8 @@
    10.4  (*For proving the easier theorems about X ~: parts (knows Spy evs).*)
    10.5  fun parts_knows_Spy_tac i = 
    10.6    EVERY
    10.7 -   [forward_tac [YM4_Key_parts_knows_Spy] (i+7),
    10.8 -    forward_tac [YM4_parts_knows_Spy] (i+6), assume_tac (i+6),
    10.9 +   [ftac YM4_Key_parts_knows_Spy (i+7),
   10.10 +    ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6),
   10.11      prove_simple_subgoals_tac i];
   10.12  
   10.13  (*Induction for regularity theorems.  If induction formula has the form
   10.14 @@ -130,7 +130,7 @@
   10.15  (*For proofs involving analz.*)
   10.16  val analz_knows_Spy_tac = 
   10.17      dtac YM4_analz_knows_Spy 7 THEN assume_tac 7 THEN
   10.18 -    forward_tac [Says_Server_message_form] 8 THEN
   10.19 +    ftac Says_Server_message_form 8 THEN
   10.20      assume_tac 8 THEN
   10.21      REPEAT ((etac conjE ORELSE' hyp_subst_tac) 8);
   10.22  
   10.23 @@ -228,7 +228,7 @@
   10.24  \        Notes Spy {|na, nb, Key K|} ~: set evs;          \
   10.25  \        A ~: bad;  B ~: bad;  evs : yahalom |]           \
   10.26  \     ==> Key K ~: analz (knows Spy evs)";
   10.27 -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   10.28 +by (ftac Says_Server_message_form 1 THEN assume_tac 1);
   10.29  by (blast_tac (claset() addSEs [lemma]) 1);
   10.30  qed "Spy_not_see_encrypted_key";
   10.31  
   10.32 @@ -372,7 +372,7 @@
   10.33  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   10.34  (*yes: delete a useless induction hypothesis; apply unicity of session keys*)
   10.35  by (thin_tac "?P-->?Q" 1);
   10.36 -by (forward_tac [Gets_imp_Says] 1 THEN assume_tac 1);
   10.37 +by (ftac Gets_imp_Says 1 THEN assume_tac 1);
   10.38  by (not_bad_tac "Aa" 1);
   10.39  by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   10.40  			addDs  [unique_session_keys]) 1);
    11.1 --- a/src/HOL/Auth/Yahalom_Bad.ML	Mon Sep 06 22:12:08 1999 +0200
    11.2 +++ b/src/HOL/Auth/Yahalom_Bad.ML	Tue Sep 07 10:40:58 1999 +0200
    11.3 @@ -35,7 +35,7 @@
    11.4  AddDs [Gets_imp_knows_Spy RS parts.Inj];
    11.5  
    11.6  fun g_not_bad_tac s = 
    11.7 -  forward_tac [Gets_imp_Says] THEN' assume_tac THEN' not_bad_tac s;
    11.8 +  ftac Gets_imp_Says THEN' assume_tac THEN' not_bad_tac s;
    11.9  
   11.10  
   11.11  (**** Inductive proofs about yahalom ****)
   11.12 @@ -55,7 +55,7 @@
   11.13  (*For proving the easier theorems about X ~: parts (knows Spy evs).*)
   11.14  fun parts_knows_Spy_tac i = 
   11.15    EVERY
   11.16 -   [forward_tac [YM4_parts_knows_Spy] (i+6), assume_tac (i+6),
   11.17 +   [ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6),
   11.18      prove_simple_subgoals_tac i];
   11.19  
   11.20  (*Induction for regularity theorems.  If induction formula has the form
   11.21 @@ -107,7 +107,7 @@
   11.22  
   11.23  (*For proofs involving analz.*)
   11.24  val analz_knows_Spy_tac = 
   11.25 -    forward_tac [YM4_analz_knows_Spy] 7 THEN assume_tac 7;
   11.26 +    ftac YM4_analz_knows_Spy 7 THEN assume_tac 7;
   11.27  
   11.28  (****
   11.29   The following is to prove theorems of the form
   11.30 @@ -291,7 +291,7 @@
   11.31  by (dtac B_trusts_YM4_newK 3);
   11.32  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   11.33  by (etac Spy_not_see_encrypted_key 1 THEN REPEAT (assume_tac 1));
   11.34 -by (forward_tac [unique_session_keys] 1 THEN REPEAT (assume_tac 1));
   11.35 +by (ftac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   11.36  by (blast_tac (claset() addDs []) 1);
   11.37  qed "B_trusts_YM4";
   11.38  
   11.39 @@ -348,7 +348,7 @@
   11.40  \          : set evs;                                                  \
   11.41  \        A ~: bad;  B ~: bad;  evs : yahalom |]       \
   11.42  \     ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   11.43 -by (forward_tac [B_trusts_YM4] 1);
   11.44 +by (ftac B_trusts_YM4 1);
   11.45  by (REPEAT_FIRST assume_tac);
   11.46  by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1);
   11.47  by (Clarify_tac 1);
    12.1 --- a/src/HOL/Divides.ML	Mon Sep 06 22:12:08 1999 +0200
    12.2 +++ b/src/HOL/Divides.ML	Tue Sep 07 10:40:58 1999 +0200
    12.3 @@ -438,14 +438,14 @@
    12.4  AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
    12.5  
    12.6  Goal "k dvd (n + k) = k dvd (n::nat)";
    12.7 -br iffI 1;
    12.8 -be  dvd_add 2;
    12.9 -br  dvd_refl 2;
   12.10 +by (rtac iffI 1);
   12.11 +by (etac dvd_add 2);
   12.12 +by (rtac dvd_refl 2);
   12.13  by (subgoal_tac "n = (n+k)-k" 1);
   12.14  by  (Simp_tac 2);
   12.15 -be ssubst 1;
   12.16 -be dvd_diff 1;
   12.17 -br dvd_refl 1;
   12.18 +by (etac ssubst 1);
   12.19 +by (etac dvd_diff 1);
   12.20 +by (rtac dvd_refl 1);
   12.21  qed "dvd_reduce";
   12.22  
   12.23  Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
    13.1 --- a/src/HOL/Finite.ML	Mon Sep 06 22:12:08 1999 +0200
    13.2 +++ b/src/HOL/Finite.ML	Tue Sep 07 10:40:58 1999 +0200
    13.3 @@ -341,7 +341,7 @@
    13.4   by (Auto_tac);
    13.5  by (asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1);
    13.6  by (Auto_tac);
    13.7 -by (forward_tac [cardR_SucD] 1);
    13.8 +by (ftac cardR_SucD 1);
    13.9  by (Blast_tac 1);
   13.10  val lemma = result();
   13.11  
   13.12 @@ -628,7 +628,7 @@
   13.13  by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] 
   13.14      (finite_imp_foldSet RS exE) 1);
   13.15  by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1);
   13.16 -by (forward_tac [Diff1_foldSet] 1 THEN assume_tac 1);
   13.17 +by (ftac Diff1_foldSet 1 THEN assume_tac 1);
   13.18  by (subgoal_tac "ya = f xb x" 1);
   13.19   by (Blast_tac 2);
   13.20  by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1);
    14.1 --- a/src/HOL/Hoare/Arith2.ML	Mon Sep 06 22:12:08 1999 +0200
    14.2 +++ b/src/HOL/Hoare/Arith2.ML	Tue Sep 07 10:40:58 1999 +0200
    14.3 @@ -36,7 +36,7 @@
    14.4  (*** gcd ***)
    14.5  
    14.6  Goalw [gcd_def] "0<n ==> n = gcd n n";
    14.7 -by (forward_tac [cd_nnn] 1);
    14.8 +by (ftac cd_nnn 1);
    14.9  by (rtac (select_equality RS sym) 1);
   14.10  by (blast_tac (claset() addDs [cd_le]) 1);
   14.11  by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1);
    15.1 --- a/src/HOL/IOA/IOA.ML	Mon Sep 06 22:12:08 1999 +0200
    15.2 +++ b/src/HOL/IOA/IOA.ML	Tue Sep 07 10:40:58 1999 +0200
    15.3 @@ -70,7 +70,7 @@
    15.4     by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    15.5    by (etac disjE 1);
    15.6     by (Asm_simp_tac 1);
    15.7 -  by (forward_tac [less_not_sym] 1);
    15.8 +  by (ftac less_not_sym 1);
    15.9    by (asm_simp_tac (simpset() addsimps [less_not_refl2,less_Suc_eq]) 1);
   15.10  qed "reachable_n";
   15.11  
    16.1 --- a/src/HOL/IOA/Solve.ML	Mon Sep 06 22:12:08 1999 +0200
    16.2 +++ b/src/HOL/IOA/Solve.ML	Tue Sep 07 10:40:58 1999 +0200
    16.3 @@ -29,7 +29,7 @@
    16.4     by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1);
    16.5  
    16.6    (* Use lemma *)
    16.7 -  by (forward_tac [states_of_exec_reachable] 1);
    16.8 +  by (ftac states_of_exec_reachable 1);
    16.9  
   16.10    (* Now show that it's an execution *)
   16.11    by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1);
    17.1 --- a/src/HOL/Induct/LFilter.ML	Mon Sep 06 22:12:08 1999 +0200
    17.2 +++ b/src/HOL/Induct/LFilter.ML	Tue Sep 07 10:40:58 1999 +0200
    17.3 @@ -47,7 +47,7 @@
    17.4  \            !!x l'. [| (l, LCons x l') : findRel p;  p x |] ==> Q    \
    17.5  \         |] ==> Q";
    17.6  by (rtac (major RS DomainE) 1);
    17.7 -by (forward_tac [findRel_imp_LCons] 1);
    17.8 +by (ftac findRel_imp_LCons 1);
    17.9  by (REPEAT (eresolve_tac [exE,conjE] 1));
   17.10  by (hyp_subst_tac 1);
   17.11  by (REPEAT (ares_tac prems 1));
   17.12 @@ -331,7 +331,7 @@
   17.13  by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3);
   17.14  by (Asm_simp_tac 2);
   17.15  by (etac Domain_findRelE 1);
   17.16 -by (forward_tac [lmap_LCons_findRel] 1);
   17.17 +by (ftac lmap_LCons_findRel 1);
   17.18  by (Clarify_tac 1);
   17.19  by (Asm_simp_tac 1);
   17.20  qed "lfilter_lmap";
    18.1 --- a/src/HOL/Induct/Multiset.ML	Mon Sep 06 22:12:08 1999 +0200
    18.2 +++ b/src/HOL/Induct/Multiset.ML	Tue Sep 07 10:40:58 1999 +0200
    18.3 @@ -307,7 +307,7 @@
    18.4   by (rtac ext 1);
    18.5   by (Force_tac 1);
    18.6  by (Clarify_tac 1);
    18.7 -by (forward_tac [setsum_SucD] 1);
    18.8 +by (ftac setsum_SucD 1);
    18.9   by (assume_tac 1);
   18.10  by (Clarify_tac 1);
   18.11  by (rename_tac "a" 1);
    19.1 --- a/src/HOL/Induct/Mutil.ML	Mon Sep 06 22:12:08 1999 +0200
    19.2 +++ b/src/HOL/Induct/Mutil.ML	Tue Sep 07 10:40:58 1999 +0200
    19.3 @@ -103,7 +103,7 @@
    19.4  by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
    19.5  by (REPEAT_FIRST assume_tac);
    19.6  (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
    19.7 -by(auto_tac (claset(), simpset() addsimps [less_Suc_eq, mod_Suc]));
    19.8 +by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, mod_Suc]));
    19.9  qed "domino_singleton";
   19.10  
   19.11  Goal "d:domino ==> finite d";
    20.1 --- a/src/HOL/Integ/IntDiv.ML	Mon Sep 06 22:12:08 1999 +0200
    20.2 +++ b/src/HOL/Integ/IntDiv.ML	Tue Sep 07 10:40:58 1999 +0200
    20.3 @@ -360,7 +360,7 @@
    20.4  qed "self_quotient";
    20.5  
    20.6  Goal "[| quorem((a,a),(q,r));  a ~= (#0::int) |] ==> r = #0";
    20.7 -by (forward_tac [self_quotient] 1);
    20.8 +by (ftac self_quotient 1);
    20.9  by (assume_tac 1);
   20.10  by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
   20.11  qed "self_remainder";
    21.1 --- a/src/HOL/MiniML/Instance.ML	Mon Sep 06 22:12:08 1999 +0200
    21.2 +++ b/src/HOL/MiniML/Instance.ML	Tue Sep 07 10:40:58 1999 +0200
    21.3 @@ -127,7 +127,7 @@
    21.4  by (simp_tac (simpset() addsimps [le_type_scheme_def2]) 1); 
    21.5  by (rtac iffI 1); 
    21.6  by (etac exE 1); 
    21.7 -by (forward_tac [bound_scheme_inst_type] 1);
    21.8 +by (ftac bound_scheme_inst_type 1);
    21.9  by (etac exE 1);
   21.10  by (rtac exI 1);
   21.11  by (rtac mk_scheme_injective 1); 
    22.1 --- a/src/HOL/MiniML/W.ML	Mon Sep 06 22:12:08 1999 +0200
    22.2 +++ b/src/HOL/MiniML/W.ML	Tue Sep 07 10:40:58 1999 +0200
    22.3 @@ -211,7 +211,7 @@
    22.4  by (asm_full_simp_tac (simpset() addsimps [rotate_Some,o_def]) 1);
    22.5  by (dtac W_var_geD 1);
    22.6  by (dtac W_var_geD 1);
    22.7 -by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
    22.8 +by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
    22.9  by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
   22.10      codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
   22.11      less_le_trans,less_not_refl2,subsetD]
   22.12 @@ -220,7 +220,7 @@
   22.13  by (Asm_full_simp_tac 1); 
   22.14  by (dtac (sym RS W_var_geD) 1);
   22.15  by (dtac (sym RS W_var_geD) 1);
   22.16 -by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
   22.17 +by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
   22.18  by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
   22.19      free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
   22.20      less_le_trans,subsetD]
   22.21 @@ -296,11 +296,11 @@
   22.22  by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   22.23  by (asm_full_simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
   22.24  by (rtac (has_type_cl_sub RS spec) 1);
   22.25 -by (forward_tac [new_tv_W] 1);
   22.26 +by (ftac new_tv_W 1);
   22.27  by (assume_tac 1);
   22.28  by (dtac conjunct1 1);
   22.29  by (dtac conjunct1 1);
   22.30 -by (forward_tac [new_tv_subst_scheme_list] 1);
   22.31 +by (ftac new_tv_subst_scheme_list 1);
   22.32  by (rtac new_scheme_list_le 1);
   22.33  by (rtac W_var_ge 1);
   22.34  by (assume_tac 1);
   22.35 @@ -340,11 +340,11 @@
   22.36  by (dres_inst_tac [("x","t")] spec 2);
   22.37  by (dres_inst_tac [("x","n2")] spec 2);
   22.38  by (dres_inst_tac [("x","m2")] spec 2);
   22.39 -by (forward_tac [new_tv_W] 2);
   22.40 +by (ftac new_tv_W 2);
   22.41  by (assume_tac 2);
   22.42  by (dtac conjunct1 2);
   22.43  by (dtac conjunct1 2);
   22.44 -by (forward_tac [new_tv_subst_scheme_list] 2);
   22.45 +by (ftac new_tv_subst_scheme_list 2);
   22.46  by (rtac new_scheme_list_le 2);
   22.47  by (rtac W_var_ge 2);
   22.48  by (assume_tac 2);
   22.49 @@ -442,7 +442,7 @@
   22.50      new_tv_not_free_tv,new_tv_le]) 3);
   22.51  by (case_tac "na:free_tv Sa" 2);
   22.52  (* n1 ~: free_tv S1 *)
   22.53 -by (forward_tac [not_free_impl_id] 3);
   22.54 +by (ftac not_free_impl_id 3);
   22.55  by (Asm_simp_tac 3);
   22.56  (* na : free_tv Sa *)
   22.57  by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
   22.58 @@ -456,7 +456,7 @@
   22.59  by (rtac eq_free_eq_subst_te 2);
   22.60  by (strip_tac 2);
   22.61  by (subgoal_tac "nb ~= ma" 2);
   22.62 -by ((forward_tac [new_tv_W] 3) THEN (atac 3));
   22.63 +by ((ftac new_tv_W 3) THEN (atac 3));
   22.64  by (etac conjE 3);
   22.65  by (dtac new_tv_subst_scheme_list 3);
   22.66  by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3);
   22.67 @@ -467,7 +467,7 @@
   22.68  by (rtac eq_free_eq_subst_te 2);
   22.69  by (strip_tac 2 );
   22.70  by (subgoal_tac "na ~= ma" 2);
   22.71 -by ((forward_tac [new_tv_W] 3) THEN (atac 3));
   22.72 +by ((ftac new_tv_W 3) THEN (atac 3));
   22.73  by (etac conjE 3);
   22.74  by (dtac (sym RS W_var_geD) 3);
   22.75  by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
   22.76 @@ -502,7 +502,7 @@
   22.77  by (rtac eq_free_eq_subst_scheme_list 1);
   22.78  by ( safe_tac HOL_cs );
   22.79  by (subgoal_tac "ma ~= na" 1);
   22.80 -by ((forward_tac [new_tv_W] 2) THEN (atac 2));
   22.81 +by ((ftac new_tv_W 2) THEN (atac 2));
   22.82  by (etac conjE 2);
   22.83  by (dtac new_tv_subst_scheme_list 2);
   22.84  by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2);
   22.85 @@ -542,7 +542,7 @@
   22.86  by (Simp_tac 1);
   22.87  by (rtac gen_bound_typ_instance 1);
   22.88  by (dtac mp 1);
   22.89 -by (forward_tac [new_tv_compatible_W] 1);
   22.90 +by (ftac new_tv_compatible_W 1);
   22.91  by (rtac sym 1);
   22.92  by (assume_tac 1);
   22.93  by (fast_tac (claset() addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
    23.1 --- a/src/HOL/Real/Hyperreal/Filter.ML	Mon Sep 06 22:12:08 1999 +0200
    23.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Tue Sep 07 10:40:58 1999 +0200
    23.3 @@ -274,7 +274,7 @@
    23.4  by (dres_inst_tac [("A","xa")] mem_FiltersetD3 2 THEN assume_tac 2);
    23.5  by (Blast_tac 2);
    23.6  by (dtac lemma_empty_Int_subset_Compl 1);
    23.7 -by (EVERY1[forward_tac [mem_Filterset_disjI], assume_tac, Fast_tac]);
    23.8 +by (EVERY1[ftac mem_Filterset_disjI , assume_tac, Fast_tac]);
    23.9  by (dtac mem_FiltersetD3 1 THEN assume_tac 1);
   23.10  by (dres_inst_tac [("x","f")] spec 1);
   23.11  by (Blast_tac 1);
   23.12 @@ -387,7 +387,7 @@
   23.13  Goalw [Ultrafilter_def,FreeUltrafilter_def]
   23.14       "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV\
   23.15  \         |] ==> {X. finite(- X)} <= U";
   23.16 -by (forward_tac [cofinite_Filter] 1);
   23.17 +by (ftac cofinite_Filter 1);
   23.18  by (Step_tac 1);
   23.19  by (forw_inst_tac [("X","- x :: 'a set")] not_finite_UNIV_Compl 1);
   23.20  by (assume_tac 1);
    24.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Sep 06 22:12:08 1999 +0200
    24.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Sep 07 10:40:58 1999 +0200
    24.3 @@ -1096,7 +1096,7 @@
    24.4  by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2);
    24.5  by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2);
    24.6  by (Auto_tac );
    24.7 -by (forward_tac [hypreal_add_order] 1 THEN assume_tac 1);
    24.8 +by (ftac hypreal_add_order 1 THEN assume_tac 1);
    24.9  by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1);
   24.10  by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   24.11  qed "hypreal_gt_zero_iff";
   24.12 @@ -1318,7 +1318,7 @@
   24.13  qed "hypreal_hrinv_gt_zero";
   24.14  
   24.15  Goal "x < 0hr ==> hrinv x < 0hr";
   24.16 -by (forward_tac [hypreal_not_refl2] 1);
   24.17 +by (ftac hypreal_not_refl2 1);
   24.18  by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
   24.19  by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
   24.20  by (dtac (hypreal_minus_hrinv RS sym) 1);
   24.21 @@ -1394,13 +1394,13 @@
   24.22  
   24.23  (* TODO: remove redundant  0hr < x *)
   24.24  Goal "[| 0hr < r; 0hr < x; r < x |] ==> hrinv x < hrinv r";
   24.25 -by (forward_tac [hypreal_hrinv_gt_zero] 1);
   24.26 +by (ftac hypreal_hrinv_gt_zero 1);
   24.27  by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1);
   24.28  by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1);
   24.29  by (assume_tac 1);
   24.30  by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
   24.31           not_sym RS hypreal_mult_hrinv]) 1);
   24.32 -by (forward_tac [hypreal_hrinv_gt_zero] 1);
   24.33 +by (ftac hypreal_hrinv_gt_zero 1);
   24.34  by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1);
   24.35  by (assume_tac 1);
   24.36  by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
    25.1 --- a/src/HOL/Real/Hyperreal/Zorn.ML	Mon Sep 06 22:12:08 1999 +0200
    25.2 +++ b/src/HOL/Real/Hyperreal/Zorn.ML	Tue Sep 07 10:40:58 1999 +0200
    25.3 @@ -177,7 +177,7 @@
    25.4  
    25.5  Goal "c: chain S - maxchain S ==> \
    25.6  \                         succ S c ~= c";
    25.7 -by (forward_tac [succI3] 1);
    25.8 +by (ftac succI3 1);
    25.9  by (Asm_simp_tac 1);
   25.10  by (rtac select_not_equals 1);
   25.11  by (assume_tac 1);
    26.1 --- a/src/HOL/Real/PReal.ML	Mon Sep 06 22:12:08 1999 +0200
    26.2 +++ b/src/HOL/Real/PReal.ML	Tue Sep 07 10:40:58 1999 +0200
    26.3 @@ -247,7 +247,7 @@
    26.4  Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
    26.5  \         !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x + y}";
    26.6  by Auto_tac;
    26.7 -by (forward_tac [prat_mult_qinv_less_1] 1);
    26.8 +by (ftac prat_mult_qinv_less_1 1);
    26.9  by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1)")] 
   26.10      prat_mult_less2_mono1 1);
   26.11  by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat 1)")] 
   26.12 @@ -658,7 +658,7 @@
   26.13  by (etac prat_lessE 1);
   26.14  by (cut_inst_tac [("R","A"),("x","Q3")] lemma_gleason9_34 1);
   26.15  by (dtac sym 1 THEN Auto_tac );
   26.16 -by (forward_tac [not_in_preal_ub] 1);
   26.17 +by (ftac not_in_preal_ub 1);
   26.18  by (dres_inst_tac [("x","xa + Q3")] bspec 1 THEN assume_tac 1);
   26.19  by (dtac prat_add_right_less_cancel 1);
   26.20  by (dres_inst_tac [("x","qinv(xa)*Q3")] prat_mult_less2_mono1 1);
    27.1 --- a/src/HOL/Real/RComplete.ML	Mon Sep 06 22:12:08 1999 +0200
    27.2 +++ b/src/HOL/Real/RComplete.ML	Tue Sep 07 10:40:58 1999 +0200
    27.3 @@ -28,7 +28,7 @@
    27.4  by (blast_tac (claset() addDs [bspec, real_gt_zero_preal_Ex RS iffD1]) 1);
    27.5  by Auto_tac;
    27.6  by (dtac bspec 1 THEN assume_tac 1);
    27.7 -by (forward_tac [bspec] 1  THEN assume_tac 1);
    27.8 +by (ftac bspec 1  THEN assume_tac 1);
    27.9  by (dtac real_less_trans 1 THEN assume_tac 1);
   27.10  by (dtac (real_gt_zero_preal_Ex RS iffD1) 1 THEN etac exE 1);
   27.11  by (res_inst_tac [("x","ya")] exI 1);
   27.12 @@ -49,22 +49,22 @@
   27.13  by (res_inst_tac 
   27.14     [("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1);
   27.15  by Auto_tac;
   27.16 -by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
   27.17 +by (ftac real_sup_lemma2 1 THEN Auto_tac);
   27.18  by (case_tac "0r < ya" 1);
   27.19  by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
   27.20  by (dtac real_less_all_real2 2);
   27.21  by Auto_tac;
   27.22  by (rtac (preal_complete RS spec RS iffD1) 1);
   27.23  by Auto_tac;
   27.24 -by (forward_tac [real_gt_preal_preal_Ex] 1);
   27.25 +by (ftac real_gt_preal_preal_Ex 1);
   27.26  by Auto_tac;
   27.27  (* second part *)
   27.28  by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
   27.29  by (case_tac "0r < ya" 1);
   27.30  by (auto_tac (claset() addSDs [real_less_all_real2,
   27.31  			       real_gt_zero_preal_Ex RS iffD1],simpset()));
   27.32 -by (forward_tac [real_sup_lemma2] 2 THEN Auto_tac);
   27.33 -by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
   27.34 +by (ftac real_sup_lemma2 2 THEN Auto_tac);
   27.35 +by (ftac real_sup_lemma2 1 THEN Auto_tac);
   27.36  by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
   27.37  by (Blast_tac 3);
   27.38  by (Blast_tac 1);
   27.39 @@ -77,7 +77,7 @@
   27.40   -------------------------------------------------------*)
   27.41  
   27.42  Goal "[| isLub R S x; isLub R S y |] ==> x = (y::real)";
   27.43 -by (forward_tac [isLub_isUb] 1);
   27.44 +by (ftac isLub_isUb 1);
   27.45  by (forw_inst_tac [("x","y")] isLub_isUb 1);
   27.46  by (blast_tac (claset() addSIs [real_le_anti_sym]
   27.47                          addSDs [isLub_le_isUb]) 1);
   27.48 @@ -105,12 +105,12 @@
   27.49  by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff]));
   27.50  by (rtac preal_psup_leI2a 1);
   27.51  by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1);
   27.52 -by (forward_tac  [real_ge_preal_preal_Ex] 1);
   27.53 +by (ftac real_ge_preal_preal_Ex 1);
   27.54  by (Step_tac 1);
   27.55  by (res_inst_tac [("x","y")] exI 1);
   27.56  by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1);
   27.57  by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1);
   27.58 -by (forward_tac [isUbD2] 1);
   27.59 +by (ftac isUbD2 1);
   27.60  by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
   27.61  by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex],
   27.62  	      simpset() addsimps [real_of_preal_le_iff]));
   27.63 @@ -188,12 +188,12 @@
   27.64  by (Step_tac 1);
   27.65  by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1);
   27.66  by (stac lemma_le_swap2 1);
   27.67 -by (forward_tac [isLubD2] 1 THEN assume_tac 2);
   27.68 +by (ftac isLubD2 1 THEN assume_tac 2);
   27.69  by (Step_tac 1);
   27.70  by (Blast_tac 1);
   27.71  by (dtac lemma_real_complete1 1 THEN REPEAT(assume_tac 1));
   27.72  by (stac lemma_le_swap2 1);
   27.73 -by (forward_tac [isLubD2] 1 THEN assume_tac 2);
   27.74 +by (ftac isLubD2 1 THEN assume_tac 2);
   27.75  by (Blast_tac 1);
   27.76  by (rtac lemma_real_complete2b 1);
   27.77  by (etac real_less_imp_le 2);
    28.1 --- a/src/HOL/Real/RealDef.ML	Mon Sep 06 22:12:08 1999 +0200
    28.2 +++ b/src/HOL/Real/RealDef.ML	Tue Sep 07 10:40:58 1999 +0200
    28.3 @@ -498,7 +498,7 @@
    28.4  qed "real_mult_inv_left_ex";
    28.5  
    28.6  Goalw [rinv_def] "x ~= 0r ==> rinv(x)*x = 1r";
    28.7 -by (forward_tac [real_mult_inv_left_ex] 1);
    28.8 +by (ftac real_mult_inv_left_ex 1);
    28.9  by (Step_tac 1);
   28.10  by (rtac selectI2 1);
   28.11  by Auto_tac;
   28.12 @@ -531,7 +531,7 @@
   28.13  qed "real_mult_right_cancel_ccontr";
   28.14  
   28.15  Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
   28.16 -by (forward_tac [real_mult_inv_left_ex] 1);
   28.17 +by (ftac real_mult_inv_left_ex 1);
   28.18  by (etac exE 1);
   28.19  by (rtac selectI2 1);
   28.20  by (auto_tac (claset(),
    29.1 --- a/src/HOL/Real/RealOrd.ML	Mon Sep 06 22:12:08 1999 +0200
    29.2 +++ b/src/HOL/Real/RealOrd.ML	Tue Sep 07 10:40:58 1999 +0200
    29.3 @@ -353,7 +353,7 @@
    29.4  qed "real_rinv_gt_zero";
    29.5  
    29.6  Goal "x < 0r ==> rinv x < 0r";
    29.7 -by (forward_tac [real_not_refl2] 1);
    29.8 +by (ftac real_not_refl2 1);
    29.9  by (dtac (real_minus_zero_less_iff RS iffD2) 1);
   29.10  by (rtac (real_minus_zero_less_iff RS iffD1) 1);
   29.11  by (dtac (real_minus_rinv RS sym) 1);
   29.12 @@ -608,14 +608,14 @@
   29.13  qed "real_of_posnat_rinv_eq_iff";
   29.14  
   29.15  Goal "[| 0r < r; r < x |] ==> rinv x < rinv r";
   29.16 -by (forward_tac [real_less_trans] 1 THEN assume_tac 1);
   29.17 -by (forward_tac [real_rinv_gt_zero] 1);
   29.18 +by (ftac real_less_trans 1 THEN assume_tac 1);
   29.19 +by (ftac real_rinv_gt_zero 1);
   29.20  by (forw_inst_tac [("x","x")] real_rinv_gt_zero 1);
   29.21  by (forw_inst_tac [("x","r"),("z","rinv r")] real_mult_less_mono1 1);
   29.22  by (assume_tac 1);
   29.23  by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS 
   29.24  					   not_sym RS real_mult_inv_right]) 1);
   29.25 -by (forward_tac [real_rinv_gt_zero] 1);
   29.26 +by (ftac real_rinv_gt_zero 1);
   29.27  by (forw_inst_tac [("x","1r"),("z","rinv x")] real_mult_less_mono2 1);
   29.28  by (assume_tac 1);
   29.29  by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS 
   29.30 @@ -704,7 +704,7 @@
   29.31  Addsimps [real_mult_eq_self_zero2];
   29.32  
   29.33  Goal "[| 0r <= x*y; 0r < x |] ==> 0r <= y";
   29.34 -by (forward_tac [real_rinv_gt_zero] 1);
   29.35 +by (ftac real_rinv_gt_zero 1);
   29.36  by (dres_inst_tac [("x","rinv x")] real_less_le_mult_order 1);
   29.37  by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2);
   29.38  by (auto_tac (claset(),
    30.1 --- a/src/HOL/Set.ML	Mon Sep 06 22:12:08 1999 +0200
    30.2 +++ b/src/HOL/Set.ML	Tue Sep 07 10:40:58 1999 +0200
    30.3 @@ -466,7 +466,7 @@
    30.4  Goal "A <= insert x B ==> A <= B & x ~: A | (? B'. A = insert x B' & B' <= B)";
    30.5  by (case_tac "x:A" 1);
    30.6  by  (Fast_tac 2);
    30.7 -br  disjI2 1;
    30.8 +by (rtac disjI2 1);
    30.9  by (res_inst_tac [("x","A-{x}")] exI 1);
   30.10  by (Fast_tac 1);
   30.11  qed "subset_insertD";
    31.1 --- a/src/HOL/Subst/UTerm.ML	Mon Sep 06 22:12:08 1999 +0200
    31.2 +++ b/src/HOL/Subst/UTerm.ML	Tue Sep 07 10:40:58 1999 +0200
    31.3 @@ -39,7 +39,7 @@
    31.4  Goal "finite(vars_of M)";
    31.5  by (induct_tac"M" 1);
    31.6  by (ALLGOALS Simp_tac);
    31.7 -by (forward_tac [finite_UnI] 1);
    31.8 +by (ftac finite_UnI 1);
    31.9  by (assume_tac 1);
   31.10  by (Asm_simp_tac 1);
   31.11  val finite_vars_of = result();
    32.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Sep 06 22:12:08 1999 +0200
    32.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 07 10:40:58 1999 +0200
    32.3 @@ -570,7 +570,7 @@
    32.4          [rtac iffI 1,
    32.5           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
    32.6           dresolve_tac rep_congs 1, dtac box_equals 1,
    32.7 -         REPEAT (resolve_tac rep_thms 1), rewrite_goals_tac [o_def],
    32.8 +         REPEAT (resolve_tac rep_thms 1), rewtac o_def,
    32.9           REPEAT (eresolve_tac inj_thms 1),
   32.10           REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1,
   32.11                    eresolve_tac inj_thms 1, atac 1]))])
   32.12 @@ -634,7 +634,7 @@
   32.13           EVERY (map (fn (prem, r) => (EVERY
   32.14             [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
   32.15              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   32.16 -            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewrite_goals_tac [o_def],
   32.17 +            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
   32.18                rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
   32.19                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   32.20  
    33.1 --- a/src/HOL/UNITY/Channel.ML	Mon Sep 06 22:12:08 1999 +0200
    33.2 +++ b/src/HOL/UNITY/Channel.ML	Tue Sep 07 10:40:58 1999 +0200
    33.3 @@ -51,7 +51,7 @@
    33.4  Goal "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}";
    33.5  by (rtac (lemma RS leadsTo_weaken_R) 1);
    33.6  by (Clarify_tac 1);
    33.7 -by (forward_tac [minSet_nonempty] 1);
    33.8 +by (ftac minSet_nonempty 1);
    33.9  by (auto_tac (claset() addDs [Suc_le_lessD, not_less_Least], 
   33.10  	      simpset()));
   33.11  qed "Channel_progress";
    34.1 --- a/src/HOL/UNITY/Extend.ML	Mon Sep 06 22:12:08 1999 +0200
    34.2 +++ b/src/HOL/UNITY/Extend.ML	Tue Sep 07 10:40:58 1999 +0200
    34.3 @@ -29,7 +29,7 @@
    34.4  val [surj,prem] = Goalw [inv_def]
    34.5       "[| surj h;  !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z";
    34.6  by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1);
    34.7 -br selectI2 1;
    34.8 +by (rtac selectI2 1);
    34.9  by (dres_inst_tac [("f", "g")] arg_cong 2);
   34.10  by (auto_tac (claset(), simpset() addsimps [prem]));
   34.11  qed "fst_inv_equalityI";
   34.12 @@ -200,9 +200,9 @@
   34.13  
   34.14  Goalw [project_set_def, project_act_def]
   34.15      "Domain (project_act h act) = project_set h (Domain act)";
   34.16 -auto();
   34.17 +by Auto_tac;
   34.18  by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1);
   34.19 -auto();
   34.20 +by Auto_tac;
   34.21  qed "Domain_project_act";
   34.22  
   34.23  Addsimps [extend_act_Id, project_act_Id];
   34.24 @@ -562,8 +562,8 @@
   34.25  Goal "F : transient (extend_set h A) ==> project h F : transient A";
   34.26  by (auto_tac (claset(),
   34.27  	      simpset() addsimps [transient_def, Domain_project_act]));
   34.28 -br bexI 1;
   34.29 -ba 2;
   34.30 +by (rtac bexI 1);
   34.31 +by (assume_tac 2);
   34.32  by (full_simp_tac (simpset() addsimps [extend_set_def, project_set_def, 
   34.33  				       project_act_def]) 1);
   34.34  by (Blast_tac 1);
   34.35 @@ -577,8 +577,8 @@
   34.36  \     ==> F : transient (extend_set h A)";
   34.37  by (auto_tac (claset(),
   34.38  	      simpset() addsimps [transient_def, 				  Domain_project_act]));
   34.39 -br bexI 1;
   34.40 -ba 2;
   34.41 +by (rtac bexI 1);
   34.42 +by (assume_tac 2);
   34.43  by Auto_tac;
   34.44  by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
   34.45  by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1);
    35.1 --- a/src/HOL/UNITY/GenPrefix.ML	Mon Sep 06 22:12:08 1999 +0200
    35.2 +++ b/src/HOL/UNITY/GenPrefix.ML	Tue Sep 07 10:40:58 1999 +0200
    35.3 @@ -136,7 +136,7 @@
    35.4  Goal "[| reflexive r;  (xs,ys) : genPrefix r |] \
    35.5  \     ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r";
    35.6  by (etac genPrefix.induct 1);
    35.7 -by (forward_tac [genPrefix_length_le] 3);
    35.8 +by (ftac genPrefix_length_le 3);
    35.9  by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2])));
   35.10  qed "genPrefix_take_append";
   35.11  
    36.1 --- a/src/HOL/UNITY/Lift_prog.ML	Mon Sep 06 22:12:08 1999 +0200
    36.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Tue Sep 07 10:40:58 1999 +0200
    36.3 @@ -507,7 +507,7 @@
    36.4  
    36.5  
    36.6  Goal "fst (inv (lift_map i) g) = g i";
    36.7 -br (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1;
    36.8 +by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1);
    36.9  by (auto_tac (claset(), simpset() addsimps [lift_map_def]));
   36.10  qed "fst_inv_lift_map";
   36.11  Addsimps [fst_inv_lift_map];
   36.12 @@ -520,34 +520,34 @@
   36.13  
   36.14  Goalw [drop_set_def, project_set_def, lift_map_def]
   36.15       "drop_set i A = project_set (lift_map i) A";
   36.16 -auto();
   36.17 -br image_eqI 2;
   36.18 -br exI 1;
   36.19 +by Auto_tac;
   36.20 +by (rtac image_eqI 2);
   36.21 +by (rtac exI 1);
   36.22  by (stac (refl RS fun_upd_idem) 1);
   36.23 -auto();
   36.24 +by Auto_tac;
   36.25  qed "drop_set_correct";
   36.26  
   36.27  Goal "lift_act i = extend_act (lift_map i)";
   36.28 -br ext 1;
   36.29 +by (rtac ext 1);
   36.30  by Auto_tac;
   36.31  by (forward_tac [good_map_lift_map RS export extend_act_D] 2);
   36.32 -by(Full_simp_tac 2);
   36.33 -bws [extend_act_def, lift_map_def];
   36.34 +by (Full_simp_tac 2);
   36.35 +by (rewrite_goals_tac [extend_act_def, lift_map_def]);
   36.36  by Auto_tac;
   36.37 -br bexI 1;
   36.38 -ba 2;
   36.39 -auto();
   36.40 -br exI 1;
   36.41 -auto();
   36.42 +by (rtac bexI 1);
   36.43 +by (assume_tac 2);
   36.44 +by Auto_tac;
   36.45 +by (rtac exI 1);
   36.46 +by Auto_tac;
   36.47  qed "lift_act_correct";
   36.48  
   36.49  Goal "drop_act i = project_act (lift_map i)";
   36.50 -br ext 1;
   36.51 -bws [project_act_def, drop_act_def, lift_map_def];
   36.52 +by (rtac ext 1);
   36.53 +by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
   36.54  by Auto_tac;
   36.55 -br image_eqI 2;
   36.56 +by (rtac image_eqI 2);
   36.57  by (REPEAT (rtac exI 1 ORELSE stac (refl RS fun_upd_idem) 1));
   36.58 -auto();
   36.59 +by Auto_tac;
   36.60  qed "drop_act_correct";
   36.61  
   36.62  
    37.1 --- a/src/HOL/W0/I.ML	Mon Sep 06 22:12:08 1999 +0200
    37.2 +++ b/src/HOL/W0/I.ML	Tue Sep 07 10:40:58 1999 +0200
    37.3 @@ -63,7 +63,7 @@
    37.4   by (etac exE 1);
    37.5   by (etac conjE 1);
    37.6   by (etac impE 1);
    37.7 -  by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
    37.8 +  by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
    37.9    by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   37.10    by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   37.11                         addss simpset()) 1);
   37.12 @@ -78,7 +78,7 @@
   37.13   by (etac exE 1);
   37.14   by (etac conjE 1);
   37.15   by (etac impE 1);
   37.16 -  by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
   37.17 +  by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
   37.18    by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   37.19    by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   37.20                         addss simpset()) 1);
   37.21 @@ -90,7 +90,7 @@
   37.22  by (etac exE 1);
   37.23  by (etac conjE 1);
   37.24  by (etac impE 1);
   37.25 - by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
   37.26 + by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
   37.27   by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   37.28   by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   37.29                        addss simpset()) 1);
   37.30 @@ -102,7 +102,7 @@
   37.31  (** LEVEL 70 **)
   37.32  by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
   37.33   by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   37.34 -by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
   37.35 +by ((ftac new_tv_subst_tel 1) THEN (atac 1));
   37.36  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   37.37  by (safe_tac HOL_cs);
   37.38    by (best_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
    38.1 --- a/src/HOL/W0/W.ML	Mon Sep 06 22:12:08 1999 +0200
    38.2 +++ b/src/HOL/W0/W.ML	Tue Sep 07 10:40:58 1999 +0200
    38.3 @@ -189,7 +189,7 @@
    38.4  by (asm_full_simp_tac (simpset() addsimps [rotate_Ok,o_def]) 1);
    38.5  by (dtac W_var_geD 1);
    38.6  by (dtac W_var_geD 1);
    38.7 -by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
    38.8 +by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
    38.9  (** LEVEL 33 **)
   38.10  by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
   38.11      codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
   38.12 @@ -199,7 +199,7 @@
   38.13  by (Asm_full_simp_tac 1); 
   38.14  by (dtac (sym RS W_var_geD) 1);
   38.15  by (dtac (sym RS W_var_geD) 1);
   38.16 -by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
   38.17 +by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
   38.18  by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
   38.19                              free_tv_app_subst_te RS subsetD,
   38.20                              free_tv_app_subst_tel RS subsetD,
   38.21 @@ -269,7 +269,7 @@
   38.22  (** LEVEL 35 **)
   38.23  by (case_tac "na:free_tv sa" 2);
   38.24  (* na ~: free_tv sa *)
   38.25 -by (forward_tac [not_free_impl_id] 3);
   38.26 +by (ftac not_free_impl_id 3);
   38.27  by (Asm_simp_tac 3);
   38.28  (* na : free_tv sa *)
   38.29  by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
   38.30 @@ -284,7 +284,7 @@
   38.31  by (rtac eq_free_eq_subst_te 2);
   38.32  by (strip_tac 2);
   38.33  by (subgoal_tac "nb ~= ma" 2);
   38.34 -by ((forward_tac [new_tv_W] 3) THEN (atac 3));
   38.35 +by ((ftac new_tv_W 3) THEN (atac 3));
   38.36  by (etac conjE 3);
   38.37  by (dtac new_tv_subst_tel 3);
   38.38  by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
   38.39 @@ -297,7 +297,7 @@
   38.40  by (rtac eq_free_eq_subst_te 2);
   38.41  by (strip_tac 2 );
   38.42  by (subgoal_tac "na ~= ma" 2);
   38.43 -by ((forward_tac [new_tv_W] 3) THEN (atac 3));
   38.44 +by ((ftac new_tv_W 3) THEN (atac 3));
   38.45  by (etac conjE 3);
   38.46  by (dtac (sym RS W_var_geD) 3);
   38.47  by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
   38.48 @@ -331,7 +331,7 @@
   38.49  by (rtac eq_free_eq_subst_tel 1);
   38.50  by ( safe_tac HOL_cs );
   38.51  by (subgoal_tac "ma ~= na" 1);
   38.52 -by ((forward_tac [new_tv_W] 2) THEN (atac 2));
   38.53 +by ((ftac new_tv_W 2) THEN (atac 2));
   38.54  by (etac conjE 2);
   38.55  by (dtac new_tv_subst_tel 2);
   38.56  by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);
    39.1 --- a/src/HOL/WF.ML	Mon Sep 06 22:12:08 1999 +0200
    39.2 +++ b/src/HOL/WF.ML	Tue Sep 07 10:40:58 1999 +0200
    39.3 @@ -326,8 +326,8 @@
    39.4  by (rtac impI 1);
    39.5  by (res_inst_tac [("a1","a")] (th RS ssubst) 1);
    39.6  by (assume_tac 1);
    39.7 -by (forward_tac [wf_trancl] 1);
    39.8 -by (forward_tac [r_into_trancl] 1);
    39.9 +by (ftac wf_trancl 1);
   39.10 +by (ftac r_into_trancl 1);
   39.11  by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1);
   39.12  by (rtac H_cong2 1);    (*expose the equality of cuts*)
   39.13  by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
    40.1 --- a/src/HOL/ex/MT.ML	Mon Sep 06 22:12:08 1999 +0200
    40.2 +++ b/src/HOL/ex/MT.ML	Tue Sep 07 10:40:58 1999 +0200
    40.3 @@ -639,7 +639,7 @@
    40.4  by (dtac elab_fix_elim 1);
    40.5  by (safe_tac HOL_cs);
    40.6  (*Do a single unfolding of cl*)
    40.7 -by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
    40.8 +by ((ftac ssubst 1) THEN (assume_tac 2));
    40.9  by (rtac hasty_rel_clos_coind 1);
   40.10  by (etac elab_fn 1);
   40.11  by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1);
    41.1 --- a/src/HOL/ex/Tarski.ML	Mon Sep 06 22:12:08 1999 +0200
    41.2 +++ b/src/HOL/ex/Tarski.ML	Tue Sep 07 10:40:58 1999 +0200
    41.3 @@ -486,7 +486,7 @@
    41.4  by (etac ssubst 1);
    41.5  by (Simp_tac 1);
    41.6  by (rtac conjI 1);
    41.7 -by (forward_tac [fixfE2] 1);
    41.8 +by (ftac fixfE2 1);
    41.9  by (etac ssubst 1);
   41.10  by (rtac reflE 1);
   41.11  by (rtac CompleteLatticeE11 1);
    42.1 --- a/src/HOLCF/Cont.ML	Mon Sep 06 22:12:08 1999 +0200
    42.2 +++ b/src/HOLCF/Cont.ML	Tue Sep 07 10:40:58 1999 +0200
    42.3 @@ -675,7 +675,7 @@
    42.4  by ( atac 1);
    42.5  by (rtac contlubI 1);
    42.6  by (strip_tac 1);
    42.7 -by (forward_tac [chfin2finch] 1);
    42.8 +by (ftac chfin2finch 1);
    42.9  by (rtac antisym_less 1);
   42.10  by ( force_tac (HOL_cs addIs [is_ub_thelub,ch2ch_monofun],
   42.11                 HOL_ss addsimps [finite_chain_def,maxinch_is_thelub]) 1);
    43.1 --- a/src/HOLCF/IOA/NTP/Correctness.ML	Mon Sep 06 22:12:08 1999 +0200
    43.2 +++ b/src/HOLCF/IOA/NTP/Correctness.ML	Tue Sep 07 10:40:58 1999 +0200
    43.3 @@ -79,19 +79,19 @@
    43.4  
    43.5  by (induct_tac "a"  1);
    43.6  by (ALLGOALS (asm_simp_tac ss'));
    43.7 -by (forward_tac [inv4] 1);
    43.8 +by (ftac inv4 1);
    43.9  by (Force_tac 1);
   43.10  
   43.11 -by (forward_tac [inv4] 1);
   43.12 -by (forward_tac [inv2] 1);
   43.13 +by (ftac inv4 1);
   43.14 +by (ftac inv2 1);
   43.15  by (etac disjE 1);
   43.16  by (Asm_simp_tac 1);
   43.17  by (Force_tac 1);
   43.18  
   43.19 -by (forward_tac [inv2] 1);
   43.20 +by (ftac inv2 1);
   43.21  by (etac disjE 1);
   43.22  
   43.23 -by (forward_tac [inv3] 1);
   43.24 +by (ftac inv3 1);
   43.25  by (case_tac "sq(sen(s))=[]" 1);
   43.26  
   43.27  by (asm_full_simp_tac ss' 1);
    44.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Sep 06 22:12:08 1999 +0200
    44.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Tue Sep 07 10:40:58 1999 +0200
    44.3 @@ -410,7 +410,7 @@
    44.4  "[| temp_strengthening P Q h |]\
    44.5  \      ==> temp_strengthening ([] P) ([] Q) h";
    44.6  by (clarify_tac set_cs 1);
    44.7 -by (forward_tac [ex2seq_tsuffix] 1);
    44.8 +by (ftac ex2seq_tsuffix 1);
    44.9  by (clarify_tac set_cs 1);
   44.10  by (dres_inst_tac [("h","h")] cex_absSeq_tsuffix 1);
   44.11  by (asm_full_simp_tac (simpset() addsimps [ex2seq_abs_cex])1);
    45.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Sep 06 22:12:08 1999 +0200
    45.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Sep 07 10:40:58 1999 +0200
    45.3 @@ -483,8 +483,8 @@
    45.4  by (safe_tac set_cs);
    45.5  
    45.6  (* Case a:A, a:B *)
    45.7 -by (forward_tac [divide_Seq] 1);
    45.8 -by (forward_tac [divide_Seq] 1);
    45.9 +by (ftac divide_Seq 1);
   45.10 +by (ftac divide_Seq 1);
   45.11  back();
   45.12  by (REPEAT (etac conjE 1));
   45.13  (* filtering internals of A in schA and of B in schB is nil *)
   45.14 @@ -501,7 +501,7 @@
   45.15                     ForallTL,ForallDropwhile]) 1);
   45.16  
   45.17  (* Case a:A, a~:B *)
   45.18 -by (forward_tac [divide_Seq] 1);
   45.19 +by (ftac divide_Seq 1);
   45.20  by (REPEAT (etac conjE 1));
   45.21  (* filtering internals of A is nil *)
   45.22  by (asm_full_simp_tac (simpset() addsimps 
   45.23 @@ -513,7 +513,7 @@
   45.24                      ForallTL,ForallDropwhile]) 1);
   45.25  
   45.26  (* Case a:B, a~:A *)
   45.27 -by (forward_tac [divide_Seq] 1);
   45.28 +by (ftac divide_Seq 1);
   45.29  by (REPEAT (etac conjE 1));
   45.30  (* filtering internals of A is nil *)
   45.31  by (asm_full_simp_tac (simpset() addsimps 
    46.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Sep 06 22:12:08 1999 +0200
    46.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Tue Sep 07 10:40:58 1999 +0200
    46.3 @@ -14,7 +14,7 @@
    46.4  \         ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A";
    46.5  by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1);
    46.6  by (safe_tac set_cs);
    46.7 -by (forward_tac  [inp_is_act] 1);
    46.8 +by (ftac inp_is_act 1);
    46.9  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   46.10  by (pair_tac "ex" 1);
   46.11  ren "s ex" 1;
   46.12 @@ -25,7 +25,7 @@
   46.13  by (assume_tac 2);
   46.14  by (etac FiniteFilter 2);
   46.15  (* subgoal 1 *)
   46.16 -by (forward_tac [exists_laststate] 1);
   46.17 +by (ftac exists_laststate 1);
   46.18  by (etac allE 1);
   46.19  by (etac exE 1);
   46.20  (* using input-enabledness *)
    47.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Sep 06 22:12:08 1999 +0200
    47.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Tue Sep 07 10:40:58 1999 +0200
    47.3 @@ -93,7 +93,7 @@
    47.4   by (dtac sym 1);
    47.5  by (Asm_full_simp_tac 1);
    47.6  by (REPEAT (hyp_subst_tac 1));
    47.7 -by (forward_tac  [reachable_rename] 1);
    47.8 +by (ftac reachable_rename 1);
    47.9  by (Asm_full_simp_tac 1);
   47.10  (* x is output *)
   47.11   by (etac exE 1);
   47.12 @@ -102,10 +102,10 @@
   47.13   by (dtac sym 1);
   47.14  by (Asm_full_simp_tac 1);
   47.15  by (REPEAT (hyp_subst_tac 1));
   47.16 -by (forward_tac  [reachable_rename] 1);
   47.17 +by (ftac reachable_rename 1);
   47.18  by (Asm_full_simp_tac 1);
   47.19  (* x is internal *)
   47.20 -by (forward_tac  [reachable_rename] 1);
   47.21 +by (ftac reachable_rename 1);
   47.22  by Auto_tac;
   47.23  qed"rename_through_pmap";
   47.24  Addsplits [split_if]; Addcongs [if_weak_cong];
    48.1 --- a/src/HOLCF/Sprod2.ML	Mon Sep 06 22:12:08 1999 +0200
    48.2 +++ b/src/HOLCF/Sprod2.ML	Tue Sep 07 10:40:58 1999 +0200
    48.3 @@ -47,7 +47,7 @@
    48.4          (strip_tac 1),
    48.5          (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
    48.6          (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
    48.7 -        (forward_tac [notUU_I] 1),
    48.8 +        (ftac notUU_I 1),
    48.9          (atac 1),
   48.10          (REPEAT(asm_simp_tac(Sprod0_ss 
   48.11                  addsimps[inst_sprod_po,refl_less,minimal]) 1))
   48.12 @@ -59,7 +59,7 @@
   48.13          (strip_tac 1),
   48.14          (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   48.15          (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
   48.16 -        (forward_tac [notUU_I] 1),
   48.17 +        (ftac notUU_I 1),
   48.18          (atac 1),
   48.19          (REPEAT(asm_simp_tac(Sprod0_ss 
   48.20                  addsimps[inst_sprod_po,refl_less,minimal]) 1))
    49.1 --- a/src/ZF/AC/AC15_WO6.ML	Mon Sep 06 22:12:08 1999 +0200
    49.2 +++ b/src/ZF/AC/AC15_WO6.ML	Tue Sep 07 10:40:58 1999 +0200
    49.3 @@ -24,7 +24,7 @@
    49.4  \       ALL x<LEAST x. HH(f,A,x)={A}. HH(f,A,x) lepoll m";
    49.5  by (rtac oallI 1);
    49.6  by (dresolve_tac [ltD RS less_Least_subset_x] 1);
    49.7 -by (forward_tac [HH_subset_imp_eq] 1);
    49.8 +by (ftac HH_subset_imp_eq 1);
    49.9  by (etac ssubst 1);
   49.10  by (fast_tac (claset() addIs [prem RS ballE]
   49.11                  addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
    50.1 --- a/src/ZF/AC/AC16_WO4.ML	Mon Sep 06 22:12:08 1999 +0200
    50.2 +++ b/src/ZF/AC/AC16_WO4.ML	Tue Sep 07 10:40:58 1999 +0200
    50.3 @@ -394,7 +394,7 @@
    50.4  by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1);
    50.5  by (EVERY (map Blast_tac [4,3,2,1]));
    50.6  by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1));
    50.7 -by (forward_tac [cons_cons_in] 1 THEN REPEAT (assume_tac 1));
    50.8 +by (ftac cons_cons_in 1 THEN REPEAT (assume_tac 1));
    50.9  by (etac ex1_two_eq 1);
   50.10  by (REPEAT (blast_tac
   50.11  	    (claset() addDs [s_subset RS subsetD, in_s_imp_u_in]) 1));
   50.12 @@ -481,8 +481,8 @@
   50.13  qed "the_in_MM_subset";
   50.14  
   50.15  Goalw [GG_def] "v : LL ==> GG ` v <= x";
   50.16 -by (forward_tac [the_in_MM_subset] 1);
   50.17 -by (forward_tac [in_LL_eq_Int] 1); 
   50.18 +by (ftac the_in_MM_subset 1);
   50.19 +by (ftac in_LL_eq_Int 1); 
   50.20  by (force_tac (claset() addEs [equalityE], simpset()) 1);
   50.21  qed "GG_subset";
   50.22  
   50.23 @@ -612,7 +612,7 @@
   50.24  by (cut_facts_tac [lemma2] 1);
   50.25  by (REPEAT (eresolve_tac [exE, conjE] 1));
   50.26  by (eres_inst_tac [("x","A Un y")] allE 1);
   50.27 -by (forward_tac [infinite_Un] 1 THEN (mp_tac 1));
   50.28 +by (ftac infinite_Un 1 THEN (mp_tac 1));
   50.29  by (etac zero_lt_natE 1); by (assume_tac 1);
   50.30  by (Clarify_tac 1);
   50.31  by (DEPTH_SOLVE (ares_tac [export conclusion] 1));
    51.1 --- a/src/ZF/AC/AC16_lemmas.ML	Mon Sep 06 22:12:08 1999 +0200
    51.2 +++ b/src/ZF/AC/AC16_lemmas.ML	Tue Sep 07 10:40:58 1999 +0200
    51.3 @@ -137,7 +137,7 @@
    51.4  by (fast_tac (claset() addSEs [Diff_sing_eqpoll,
    51.5                  Diff_sing_eqpoll RS eqpoll_succ_imp_not_empty]) 1);
    51.6  by (resolve_tac [Union_eq_Un RSN (2, subst_elem)] 1 THEN (assume_tac 2));
    51.7 -by (forward_tac [bspec] 1 THEN (assume_tac 1));
    51.8 +by (ftac bspec 1 THEN (assume_tac 1));
    51.9  by (dresolve_tac [Diff_subset RS subsetD RSN (2, bspec)] 1 THEN (assume_tac 1));
   51.10  by (dtac Un_Ord_disj 1 THEN (assume_tac 1));
   51.11  by (etac DiffE 1);
    52.1 --- a/src/ZF/AC/AC2_AC6.ML	Mon Sep 06 22:12:08 1999 +0200
    52.2 +++ b/src/ZF/AC/AC2_AC6.ML	Tue Sep 07 10:40:58 1999 +0200
    52.3 @@ -138,7 +138,7 @@
    52.4  by (rtac ballI 1);
    52.5  by (rtac apply_equality 1 THEN (assume_tac 2));
    52.6  by (etac domainE 1);
    52.7 -by (forward_tac [range_type] 1 THEN (assume_tac 1));
    52.8 +by (ftac range_type 1 THEN (assume_tac 1));
    52.9  by (fast_tac (claset() addDs [apply_equality]) 1);
   52.10  qed "AC4_AC5";
   52.11  
   52.12 @@ -164,7 +164,7 @@
   52.13  
   52.14  Goal "[| EX f: A->C. P(f,domain(f)); A=B |] ==>  EX f: B->C. P(f,B)";
   52.15  by (etac bexE 1);
   52.16 -by (forward_tac [domain_of_fun] 1);
   52.17 +by (ftac domain_of_fun 1);
   52.18  by (Fast_tac 1);
   52.19  val lemma3 = result();
   52.20  
    53.1 --- a/src/ZF/AC/AC_Equiv.ML	Mon Sep 06 22:12:08 1999 +0200
    53.2 +++ b/src/ZF/AC/AC_Equiv.ML	Tue Sep 07 10:40:58 1999 +0200
    53.3 @@ -36,8 +36,8 @@
    53.4  goal Cardinal.thy
    53.5       "!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m";
    53.6  by (rtac not_emptyE 1 THEN (assume_tac 1));
    53.7 -by (forward_tac [singleton_subsetI] 1);
    53.8 -by (forward_tac [subsetD] 1 THEN (assume_tac 1));
    53.9 +by (ftac singleton_subsetI 1);
   53.10 +by (ftac subsetD 1 THEN (assume_tac 1));
   53.11  by (res_inst_tac [("A2","A")] 
   53.12       (Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 
   53.13      THEN (REPEAT (assume_tac 2)));
    54.1 --- a/src/ZF/AC/DC.ML	Mon Sep 06 22:12:08 1999 +0200
    54.2 +++ b/src/ZF/AC/DC.ML	Tue Sep 07 10:40:58 1999 +0200
    54.3 @@ -214,7 +214,7 @@
    54.4  by (etac conjE 1);
    54.5  by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1
    54.6          THEN (assume_tac 1));
    54.7 -by (forward_tac [Diff_sing_eqpoll] 1 THEN (assume_tac 1));
    54.8 +by (ftac Diff_sing_eqpoll 1 THEN (assume_tac 1));
    54.9  by (etac allE 1);
   54.10  by (etac impE 1);
   54.11  by (Fast_tac 1);
    55.1 --- a/src/ZF/AC/DC_lemmas.ML	Mon Sep 06 22:12:08 1999 +0200
    55.2 +++ b/src/ZF/AC/DC_lemmas.ML	Tue Sep 07 10:40:58 1999 +0200
    55.3 @@ -97,7 +97,7 @@
    55.4  qed "restrict_eq_imp_val_eq";
    55.5  
    55.6  Goal "[| domain(f)=A; f:B->C |] ==> f:A->C";
    55.7 -by (forward_tac [domain_of_fun] 1);
    55.8 +by (ftac domain_of_fun 1);
    55.9  by (Fast_tac 1);
   55.10  qed "domain_eq_imp_fun_type";
   55.11  
    56.1 --- a/src/ZF/AC/HH.ML	Mon Sep 06 22:12:08 1999 +0200
    56.2 +++ b/src/ZF/AC/HH.ML	Tue Sep 07 10:40:58 1999 +0200
    56.3 @@ -186,7 +186,7 @@
    56.4  Goal "[| f : (Pow(x)-{0}) -> {{z}. z:x};  \
    56.5  \       a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}";
    56.6  by (dtac less_Least_subset_x 1);
    56.7 -by (forward_tac [HH_subset_imp_eq] 1);
    56.8 +by (ftac HH_subset_imp_eq 1);
    56.9  by (dtac apply_type 1);
   56.10  by (resolve_tac [Diff_subset RS PowI RS DiffI] 1);
   56.11  by (fast_tac 
    57.1 --- a/src/ZF/AC/WO1_WO7.ML	Mon Sep 06 22:12:08 1999 +0200
    57.2 +++ b/src/ZF/AC/WO1_WO7.ML	Tue Sep 07 10:40:58 1999 +0200
    57.3 @@ -72,7 +72,7 @@
    57.4  by (REPEAT (resolve_tac [allI,impI] 1));
    57.5  by (REPEAT (eresolve_tac [allE,exE] 1));
    57.6  by (REPEAT (ares_tac [exI,conjI,notI] 1));
    57.7 -by (forward_tac [well_ord_converse_Memrel] 1 THEN (assume_tac 1));
    57.8 +by (ftac well_ord_converse_Memrel 1 THEN (assume_tac 1));
    57.9  by (forward_tac [Ord_ordertype RS converse_Memrel_not_well_ord] 1);
   57.10  by (contr_tac 2);
   57.11  by (fast_tac (empty_cs addSEs [ordertype_ord_iso RS ord_iso_is_bij RS 
    58.1 --- a/src/ZF/AC/WO2_AC16.ML	Mon Sep 06 22:12:08 1999 +0200
    58.2 +++ b/src/ZF/AC/WO2_AC16.ML	Tue Sep 07 10:40:58 1999 +0200
    58.3 @@ -404,7 +404,7 @@
    58.4          THEN (assume_tac 1));
    58.5  by (forward_tac [subsetD RS Diff_sing_lepoll] 1
    58.6          THEN REPEAT (assume_tac 1));
    58.7 -by (forward_tac [lepoll_Diff_sing] 1);
    58.8 +by (ftac lepoll_Diff_sing 1);
    58.9  by (REPEAT (eresolve_tac [allE, impE] 1));
   58.10  by (rtac conjI 1);
   58.11  by (Fast_tac 2);
   58.12 @@ -443,7 +443,7 @@
   58.13  by (eresolve_tac [dbl_Diff_eqpoll RS ex_subset_eqpoll RS bexE] 1
   58.14          THEN REPEAT (assume_tac 1));
   58.15  by (etac Card_is_Ord 1);
   58.16 -by (forward_tac [Un_in_Collect] 2 THEN REPEAT (assume_tac 2));
   58.17 +by (ftac Un_in_Collect 2 THEN REPEAT (assume_tac 2));
   58.18  by (etac CollectE 4);
   58.19  by (rtac bexI 4);
   58.20  by (rtac CollectI 5);
   58.21 @@ -521,7 +521,7 @@
   58.22  \       (ALL x<a. x < b | (EX Y:recfunAC16(f, fa, b, a). fa ` x <= Y) -->  \
   58.23  \       (EX! Y. Y:recfunAC16(f, fa, b, a) & fa ` x <= Y))";
   58.24  by (etac lt_induct 1);
   58.25 -by (forward_tac [lt_Ord] 1);
   58.26 +by (ftac lt_Ord 1);
   58.27  by (etac Ord_cases 1);
   58.28  (* case 0 *)
   58.29  by (asm_simp_tac (simpset() addsimps [recfunAC16_0]) 1);
   58.30 @@ -568,7 +568,7 @@
   58.31  by (etac imageE 1);
   58.32  by (dresolve_tac [prem3 RS Limit_is_Ord RSN (2, ltI) RS
   58.33          (prem3 RS Limit_has_succ)] 1);
   58.34 -by (forward_tac [prem1] 1);
   58.35 +by (ftac prem1 1);
   58.36  by (etac conjE 1);
   58.37  (** LEVEL 10 **)
   58.38  by (dresolve_tac [leI RS succ_leE RSN (2, ospec)] 1 THEN (assume_tac 1));
   58.39 @@ -585,8 +585,8 @@
   58.40  by (dresolve_tac [prem4 RS subsetD] 2 THEN (assume_tac 2));
   58.41  (** LEVEL 20 **)
   58.42  by (fast_tac FOL_cs 2);
   58.43 -by (forward_tac [prem1] 1);
   58.44 -by (forward_tac [succ_leE] 1);
   58.45 +by (ftac prem1 1);
   58.46 +by (ftac succ_leE 1);
   58.47  by (dresolve_tac [prem4 RS subsetD] 1 THEN (assume_tac 1));
   58.48  by (etac conjE 1);
   58.49  (** LEVEL 25 **)
   58.50 @@ -604,11 +604,11 @@
   58.51  Goalw [AC16_def] "[| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)";
   58.52  by (rtac allI 1);
   58.53  by (rtac impI 1);
   58.54 -by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1 
   58.55 +by (ftac WO2_infinite_subsets_eqpoll_X 1 
   58.56      THEN (REPEAT (assume_tac 1)));
   58.57  by (forw_inst_tac [("n","k #+ m")] (WO2_infinite_subsets_eqpoll_X) 1
   58.58          THEN (REPEAT (ares_tac [add_type] 1)));
   58.59 -by (forward_tac [WO2_imp_ex_Card] 1);
   58.60 +by (ftac WO2_imp_ex_Card 1);
   58.61  by (REPEAT (eresolve_tac [exE,conjE] 1));
   58.62  by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS
   58.63          def_imp_iff RS iffD1)] 1 THEN (assume_tac 1));
    59.1 --- a/src/ZF/AC/WO6_WO1.ML	Mon Sep 06 22:12:08 1999 +0200
    59.2 +++ b/src/ZF/AC/WO6_WO1.ML	Tue Sep 07 10:40:58 1999 +0200
    59.3 @@ -453,7 +453,7 @@
    59.4  by (dtac WO6_imp_NN_not_empty 1);
    59.5  by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1);
    59.6  by (eres_inst_tac [("A","NN(y)")] not_emptyE 1);
    59.7 -by (forward_tac [y_well_ord] 1);
    59.8 +by (ftac y_well_ord 1);
    59.9  by (fast_tac (claset() addEs [well_ord_subset]) 2);
   59.10  by (fast_tac (claset() addSIs [lemma3] addSDs [NN_y_0] addSEs [not_emptyE]) 1);
   59.11  qed "WO6_imp_WO1";
    60.1 --- a/src/ZF/Arith.ML	Mon Sep 06 22:12:08 1999 +0200
    60.2 +++ b/src/ZF/Arith.ML	Tue Sep 07 10:40:58 1999 +0200
    60.3 @@ -200,7 +200,7 @@
    60.4  
    60.5  (*Addition is the inverse of subtraction*)
    60.6  Goal "[| n le m;  m:nat |] ==> n #+ (m#-n) = m";
    60.7 -by (forward_tac [lt_nat_in_nat] 1);
    60.8 +by (ftac lt_nat_in_nat 1);
    60.9  by (etac nat_succI 1);
   60.10  by (etac rev_mp 1);
   60.11  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   60.12 @@ -208,14 +208,14 @@
   60.13  qed "add_diff_inverse";
   60.14  
   60.15  Goal "[| n le m;  m:nat |] ==> (m#-n) #+ n = m";
   60.16 -by (forward_tac [lt_nat_in_nat] 1);
   60.17 +by (ftac lt_nat_in_nat 1);
   60.18  by (etac nat_succI 1);
   60.19  by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
   60.20  qed "add_diff_inverse2";
   60.21  
   60.22  (*Proof is IDENTICAL to that above*)
   60.23  Goal "[| n le m;  m:nat |] ==> succ(m) #- n = succ(m#-n)";
   60.24 -by (forward_tac [lt_nat_in_nat] 1);
   60.25 +by (ftac lt_nat_in_nat 1);
   60.26  by (etac nat_succI 1);
   60.27  by (etac rev_mp 1);
   60.28  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   60.29 @@ -272,7 +272,7 @@
   60.30  (*** Remainder ***)
   60.31  
   60.32  Goal "[| 0<n;  n le m;  m:nat |] ==> m #- n < m";
   60.33 -by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   60.34 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   60.35  by (etac rev_mp 1);
   60.36  by (etac rev_mp 1);
   60.37  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   60.38 @@ -299,7 +299,7 @@
   60.39  qed "mod_less";
   60.40  
   60.41  Goal "[| 0<n;  n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
   60.42 -by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   60.43 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   60.44  by (rtac (mod_def RS def_transrec RS trans) 1);
   60.45  by (asm_simp_tac div_ss 1);
   60.46  qed "mod_geq";
   60.47 @@ -321,7 +321,7 @@
   60.48  qed "div_less";
   60.49  
   60.50  Goal "[| 0<n;  n le m;  m:nat |] ==> m div n = succ((m#-n) div n)";
   60.51 -by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   60.52 +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   60.53  by (rtac (div_def RS def_transrec RS trans) 1);
   60.54  by (asm_simp_tac div_ss 1);
   60.55  qed "div_geq";
   60.56 @@ -408,7 +408,7 @@
   60.57  
   60.58  (*strict, in 1st argument; proof is by rule induction on 'less than'*)
   60.59  Goal "[| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
   60.60 -by (forward_tac [lt_nat_in_nat] 1);
   60.61 +by (ftac lt_nat_in_nat 1);
   60.62  by (assume_tac 1);
   60.63  by (etac succ_lt_induct 1);
   60.64  by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
   60.65 @@ -453,7 +453,7 @@
   60.66  (*** Monotonicity of Multiplication ***)
   60.67  
   60.68  Goal "[| i le j; j:nat; k:nat |] ==> i#*k le j#*k";
   60.69 -by (forward_tac [lt_nat_in_nat] 1);
   60.70 +by (ftac lt_nat_in_nat 1);
   60.71  by (induct_tac "k" 2);
   60.72  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
   60.73  qed "mult_le_mono1";
   60.74 @@ -471,7 +471,7 @@
   60.75  (*strict, in 1st argument; proof is by induction on k>0*)
   60.76  Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
   60.77  by (etac zero_lt_natE 1);
   60.78 -by (forward_tac [lt_nat_in_nat] 2);
   60.79 +by (ftac lt_nat_in_nat 2);
   60.80  by (ALLGOALS Asm_simp_tac);
   60.81  by (induct_tac "x" 1);
   60.82  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
   60.83 @@ -534,7 +534,7 @@
   60.84  qed "add_le_elim1";
   60.85  
   60.86  Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
   60.87 -by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
   60.88 +by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   60.89  by (etac rev_mp 1);
   60.90  by (induct_tac "n" 1);
   60.91  by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
    61.1 --- a/src/ZF/Cardinal.ML	Mon Sep 06 22:12:08 1999 +0200
    61.2 +++ b/src/ZF/Cardinal.ML	Tue Sep 07 10:40:58 1999 +0200
    61.3 @@ -650,7 +650,7 @@
    61.4  qed "Diff_sing_eqpoll";
    61.5  
    61.6  Goal "[| A lepoll 1; a:A |] ==> A = {a}";
    61.7 -by (forward_tac [Diff_sing_lepoll] 1);
    61.8 +by (ftac Diff_sing_lepoll 1);
    61.9  by (assume_tac 1);
   61.10  by (dtac lepoll_0_is_0 1);
   61.11  by (blast_tac (claset() addEs [equalityE]) 1);
    62.1 --- a/src/ZF/CardinalArith.ML	Mon Sep 06 22:12:08 1999 +0200
    62.2 +++ b/src/ZF/CardinalArith.ML	Tue Sep 07 10:40:58 1999 +0200
    62.3 @@ -357,7 +357,7 @@
    62.4  (*Kunen's Lemma 10.11*)
    62.5  Goalw [InfCard_def] "InfCard(K) ==> Limit(K)";
    62.6  by (etac conjE 1);
    62.7 -by (forward_tac [Card_is_Ord] 1);
    62.8 +by (ftac Card_is_Ord 1);
    62.9  by (rtac (ltI RS non_succ_LimitI) 1);
   62.10  by (etac ([asm_rl, nat_0I] MRS (le_imp_subset RS subsetD)) 1);
   62.11  by (safe_tac (claset() addSDs [Limit_nat RS Limit_le_succD]));
    63.1 --- a/src/ZF/Coind/MT.ML	Mon Sep 06 22:12:08 1999 +0200
    63.2 +++ b/src/ZF/Coind/MT.ML	Tue Sep 07 10:40:58 1999 +0200
    63.3 @@ -46,7 +46,7 @@
    63.4  \  <cl,t>:HasTyRel";
    63.5  by (etac elab_fixE 1);
    63.6  by Safe_tac;
    63.7 -by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]);
    63.8 +by (EVERY [ftac subst 1,atac 2,rtac htr_closCI 1]);
    63.9  by clean_tac;
   63.10  by (rtac ve_owrI 1);
   63.11  by clean_tac;
    64.1 --- a/src/ZF/Coind/Map.ML	Mon Sep 06 22:12:08 1999 +0200
    64.2 +++ b/src/ZF/Coind/Map.ML	Tue Sep 07 10:40:58 1999 +0200
    64.3 @@ -134,7 +134,7 @@
    64.4  
    64.5  Goalw [PMap_def]
    64.6    "[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
    64.7 -by (forward_tac [tmap_app_notempty] 1); 
    64.8 +by (ftac tmap_app_notempty 1); 
    64.9  by (assume_tac 1);
   64.10  by (dtac tmap_appI 1); 
   64.11  by (assume_tac 1);
    65.1 --- a/src/ZF/IMP/Equiv.ML	Mon Sep 06 22:12:08 1999 +0200
    65.2 +++ b/src/ZF/IMP/Equiv.ML	Tue Sep 07 10:40:58 1999 +0200
    65.3 @@ -79,7 +79,7 @@
    65.4  (* while *)
    65.5  by Safe_tac;
    65.6  by (ALLGOALS Asm_full_simp_tac);
    65.7 -by (EVERY1 [forward_tac [Gamma_bnd_mono], etac induct, atac]);
    65.8 +by (EVERY1 [ftac Gamma_bnd_mono , etac induct, atac]);
    65.9  by (rewtac Gamma_def);  
   65.10  by Safe_tac;
   65.11  by (EVERY1 [dtac bspec, atac]);
    66.1 --- a/src/ZF/Order.ML	Mon Sep 06 22:12:08 1999 +0200
    66.2 +++ b/src/ZF/Order.ML	Tue Sep 07 10:40:58 1999 +0200
    66.3 @@ -374,8 +374,8 @@
    66.4  (*Simple consequence of Lemma 6.1*)
    66.5  Goal "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);  \
    66.6  \        a:A;  c:A |] ==> a=c";
    66.7 -by (forward_tac [well_ord_is_trans_on] 1);
    66.8 -by (forward_tac [well_ord_is_linear] 1);
    66.9 +by (ftac well_ord_is_trans_on 1);
   66.10 +by (ftac well_ord_is_linear 1);
   66.11  by (linear_case_tac 1);
   66.12  by (dtac ord_iso_sym 1);
   66.13  (*two symmetric cases*)
   66.14 @@ -422,7 +422,7 @@
   66.15  by (Asm_simp_tac 1);
   66.16  by (rtac well_ord_iso_pred_eq 1);
   66.17  by (REPEAT_SOME assume_tac);
   66.18 -by (forward_tac [ord_iso_restrict_pred] 1  THEN
   66.19 +by (ftac ord_iso_restrict_pred 1  THEN
   66.20      REPEAT1 (eresolve_tac [asm_rl, predI] 1));
   66.21  by (asm_full_simp_tac
   66.22      (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
   66.23 @@ -437,11 +437,11 @@
   66.24  Goal "[| well_ord(A,r);  \
   66.25  \            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |] \
   66.26  \         ==> ~ <g`y, f`y> : s";
   66.27 -by (forward_tac [well_ord_iso_subset_lemma] 1);
   66.28 +by (ftac well_ord_iso_subset_lemma 1);
   66.29  by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1);
   66.30  by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));
   66.31  by Safe_tac;
   66.32 -by (forward_tac [ord_iso_converse] 1);
   66.33 +by (ftac ord_iso_converse 1);
   66.34  by (EVERY (map (blast_tac bij_apply_cs) [1,1,1]));
   66.35  by (asm_full_simp_tac bij_inverse_ss 1);
   66.36  qed "well_ord_iso_unique_lemma";
   66.37 @@ -535,7 +535,7 @@
   66.38  (*Harder case: <a, xa>: r*)
   66.39  by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1  THEN
   66.40      REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));
   66.41 -by (forward_tac [ord_iso_restrict_pred] 1  THEN
   66.42 +by (ftac ord_iso_restrict_pred 1  THEN
   66.43      REPEAT1 (eresolve_tac [asm_rl, predI] 1));
   66.44  by (asm_full_simp_tac
   66.45      (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
   66.46 @@ -546,7 +546,7 @@
   66.47  Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
   66.48  \       domain(ord_iso_map(A,r,B,s)) = A |      \
   66.49  \       (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))";
   66.50 -by (forward_tac [well_ord_is_wf] 1);
   66.51 +by (ftac well_ord_is_wf 1);
   66.52  by (rewrite_goals_tac [wf_on_def, wf_def]);
   66.53  by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1);
   66.54  by Safe_tac;
    67.1 --- a/src/ZF/OrderType.ML	Mon Sep 06 22:12:08 1999 +0200
    67.2 +++ b/src/ZF/OrderType.ML	Tue Sep 07 10:40:58 1999 +0200
    67.3 @@ -39,7 +39,7 @@
    67.4  qed "pred_Memrel";
    67.5  
    67.6  Goal "[| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
    67.7 -by (forward_tac [lt_pred_Memrel] 1);
    67.8 +by (ftac lt_pred_Memrel 1);
    67.9  by (etac ltE 1);
   67.10  by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
   67.11      assume_tac 3 THEN assume_tac 1);
   67.12 @@ -167,7 +167,7 @@
   67.13  
   67.14  Goal "[| f: ord_iso(A,r,B,s);  well_ord(B,s) |] ==> \
   67.15  \    ordertype(A,r) = ordertype(B,s)";
   67.16 -by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1);
   67.17 +by (ftac well_ord_ord_iso 1 THEN assume_tac 1);
   67.18  by (rtac Ord_iso_implies_eq 1
   67.19      THEN REPEAT (etac Ord_ordertype 1));
   67.20  by (deepen_tac (claset() addIs  [ord_iso_trans, ord_iso_sym]
   67.21 @@ -535,8 +535,8 @@
   67.22  qed "oadd_le_self2";
   67.23  
   67.24  Goal "[| k le j;  Ord(i) |] ==> k++i le j++i";
   67.25 -by (forward_tac [lt_Ord] 1);
   67.26 -by (forward_tac [le_Ord2] 1);
   67.27 +by (ftac lt_Ord 1);
   67.28 +by (ftac le_Ord2 1);
   67.29  by (etac trans_induct3 1);
   67.30  by (Asm_simp_tac 1);
   67.31  by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_le_iff]) 1);
   67.32 @@ -818,8 +818,8 @@
   67.33  qed "omult_le_self";
   67.34  
   67.35  Goal "[| k le j;  Ord(i) |] ==> k**i le j**i";
   67.36 -by (forward_tac [lt_Ord] 1);
   67.37 -by (forward_tac [le_Ord2] 1);
   67.38 +by (ftac lt_Ord 1);
   67.39 +by (ftac le_Ord2 1);
   67.40  by (etac trans_induct3 1);
   67.41  by (asm_simp_tac (simpset() addsimps [le_refl, Ord_0]) 1);
   67.42  by (asm_simp_tac (simpset() addsimps [omult_succ, oadd_le_mono]) 1);
   67.43 @@ -856,7 +856,7 @@
   67.44  qed "omult_lt_mono";
   67.45  
   67.46  Goal "[| Ord(i);  0<j |] ==> i le j**i";
   67.47 -by (forward_tac [lt_Ord2] 1);
   67.48 +by (ftac lt_Ord2 1);
   67.49  by (eres_inst_tac [("i","i")] trans_induct3 1);
   67.50  by (asm_simp_tac (simpset() addsimps [omult_0, Ord_0 RS le_refl]) 1);
   67.51  by (asm_simp_tac (simpset() addsimps [omult_succ, succ_le_iff]) 1);
    68.1 --- a/src/ZF/Resid/Confluence.ML	Mon Sep 06 22:12:08 1999 +0200
    68.2 +++ b/src/ZF/Resid/Confluence.ML	Tue Sep 07 10:40:58 1999 +0200
    68.3 @@ -38,7 +38,7 @@
    68.4  
    68.5  Goalw [confluence_def] "confluence(Spar_red1)";
    68.6  by (Clarify_tac 1);
    68.7 -by (forward_tac [simulation] 1);
    68.8 +by (ftac simulation 1);
    68.9  by (forw_inst_tac [("n","z")] simulation 1);
   68.10  by (Clarify_tac 1);
   68.11  by (forw_inst_tac [("v","va")] paving 1);
    69.1 --- a/src/ZF/Resid/Substitution.ML	Mon Sep 06 22:12:08 1999 +0200
    69.2 +++ b/src/ZF/Resid/Substitution.ML	Tue Sep 07 10:40:58 1999 +0200
    69.3 @@ -131,7 +131,7 @@
    69.4  by (ALLGOALS Asm_simp_tac);
    69.5  by Safe_tac;
    69.6  by (case_tac "n < xa" 1);
    69.7 -by ((forward_tac [lt_trans2] 1) THEN (assume_tac 1));
    69.8 +by ((ftac lt_trans2 1) THEN (assume_tac 1));
    69.9  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
   69.10  qed "lift_lift_rec";
   69.11  
   69.12 @@ -176,7 +176,7 @@
   69.13  by (excluded_middle_tac "n < x" 1);
   69.14  by (Asm_full_simp_tac 1);
   69.15  by (eres_inst_tac [("i","x")] leE 1);
   69.16 -by (forward_tac  [lt_trans1] 1 THEN assume_tac 1);
   69.17 +by (ftac lt_trans1 1 THEN assume_tac 1);
   69.18  by (ALLGOALS(asm_simp_tac 
   69.19               (simpset() addsimps [succ_pred,leI,gt_pred])));
   69.20  by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
   69.21 @@ -218,7 +218,7 @@
   69.22  by (eres_inst_tac [("j","n")] leE 1);
   69.23  by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
   69.24  by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1);
   69.25 -by (forward_tac [lt_trans2] 1 THEN assume_tac 1);
   69.26 +by (ftac lt_trans2 1 THEN assume_tac 1);
   69.27  by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
   69.28  qed "subst_rec_subst_rec";
   69.29  
    70.1 --- a/src/ZF/Zorn.ML	Mon Sep 06 22:12:08 1999 +0200
    70.2 +++ b/src/ZF/Zorn.ML	Tue Sep 07 10:40:58 1999 +0200
    70.3 @@ -300,7 +300,7 @@
    70.4  by (Blast_tac 2);
    70.5  (*Now prove the well_foundedness goal*)
    70.6  by (rtac wf_onI 1);
    70.7 -by (forward_tac [well_ord_TFin_lemma] 1 THEN assume_tac 1);
    70.8 +by (ftac well_ord_TFin_lemma 1 THEN assume_tac 1);
    70.9  by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1);
   70.10  by (Blast_tac 1);
   70.11  qed "well_ord_TFin";
    71.1 --- a/src/ZF/ex/Primrec.ML	Mon Sep 06 22:12:08 1999 +0200
    71.2 +++ b/src/ZF/ex/Primrec.ML	Tue Sep 07 10:40:58 1999 +0200
    71.3 @@ -75,7 +75,7 @@
    71.4  
    71.5  (*PROPERTY A 5, monotonicity for < *)
    71.6  Goal "[| j<k; i:nat; k:nat |] ==> ack(i,j) < ack(i,k)";
    71.7 -by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
    71.8 +by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
    71.9  by (etac succ_lt_induct 1);
   71.10  by (assume_tac 1);
   71.11  by (rtac lt_trans 2);
   71.12 @@ -106,7 +106,7 @@
   71.13  
   71.14  (*PROPERTY A 7, monotonicity for < *)
   71.15  Goal "[| i<j; j:nat; k:nat |] ==> ack(i,k) < ack(j,k)";
   71.16 -by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
   71.17 +by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   71.18  by (etac succ_lt_induct 1);
   71.19  by (assume_tac 1);
   71.20  by (rtac lt_trans 2);
   71.21 @@ -227,7 +227,7 @@
   71.22  \                       f`l < ack(kf, list_add(l))})            \
   71.23  \      |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l < ack(k, list_add(l))";
   71.24  by (Asm_simp_tac 1);
   71.25 -by (forward_tac [list_CollectD] 1);
   71.26 +by (ftac list_CollectD 1);
   71.27  by (etac (COMP_map_lemma RS bexE) 1);
   71.28  by (rtac (ballI RS bexI) 1);
   71.29  by (etac (bspec RS lt_trans) 1);
    72.1 --- a/src/ZF/ex/Term.ML	Mon Sep 06 22:12:08 1999 +0200
    72.2 +++ b/src/ZF/ex/Term.ML	Tue Sep 07 10:40:58 1999 +0200
    72.3 @@ -93,7 +93,7 @@
    72.4  \                 ==> d(x, zs, r): C(Apply(x,zs))       \
    72.5  \    |] ==> term_rec(t,d) : C(t)";
    72.6  by (rtac (major RS term.induct) 1);
    72.7 -by (forward_tac [list_CollectD] 1);
    72.8 +by (ftac list_CollectD 1);
    72.9  by (stac term_rec 1);
   72.10  by (REPEAT (ares_tac prems 1));
   72.11  by (etac list.induct 1);
    73.1 --- a/src/ZF/func.ML	Mon Sep 06 22:12:08 1999 +0200
    73.2 +++ b/src/ZF/func.ML	Tue Sep 07 10:40:58 1999 +0200
    73.3 @@ -89,7 +89,7 @@
    73.4  qed "apply_0";
    73.5  
    73.6  Goal "[| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>";
    73.7 -by (forward_tac [fun_is_rel] 1);
    73.8 +by (ftac fun_is_rel 1);
    73.9  by (blast_tac (claset() addDs [apply_equality]) 1);
   73.10  qed "Pi_memberD";
   73.11  
   73.12 @@ -112,7 +112,7 @@
   73.13  qed "apply_funtype";
   73.14  
   73.15  Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
   73.16 -by (forward_tac [fun_is_rel] 1);
   73.17 +by (ftac fun_is_rel 1);
   73.18  by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1);
   73.19  qed "apply_iff";
   73.20