src/HOL/Auth/OtwayRees_Bad.ML

           OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
 
 (*For proving the easier theorems about X ~: parts (knows Spy evs).*)
 fun parts_induct_tac i = 
     etac otway.induct i			THEN 
-    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
-    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
-    forward_tac [OR2_parts_knows_Spy]  (i+4) THEN 
+    ftac Oops_parts_knows_Spy (i+7) THEN
+    ftac OR4_parts_knows_Spy (i+6) THEN
+    ftac OR2_parts_knows_Spy (i+4) THEN 
     prove_simple_subgoals_tac  i;
 
 
 (** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
     sends messages containing X! **)

 
 (*For proofs involving analz.*)
 val analz_knows_Spy_tac = 
     dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN 
     dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
-    forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
+    ftac Says_Server_message_form 8 THEN assume_tac 8 THEN
     REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
 
 
 (****
  The following is to prove theorems of the form

 \         {|NA, Crypt (shrK A) {|NA, Key K|},                    \
 \               Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
 \        Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
 \        A ~: bad;  B ~: bad;  evs : otway |]                    \
 \     ==> Key K ~: analz (knows Spy evs)";
-by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
+by (ftac Says_Server_message_form 1 THEN assume_tac 1);
 by (blast_tac (claset() addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
 
 
 (*** Attempting to prove stronger properties ***)