src/Pure/tactic.ML

   val biresolve_tac: Proof.context -> (bool * thm) list -> int -> tactic
   val resolve0_tac: thm list -> int -> tactic
   val resolve_tac: Proof.context -> thm list -> int -> tactic
   val eresolve0_tac: thm list -> int -> tactic
   val eresolve_tac: Proof.context -> thm list -> int -> tactic
-  val forward0_tac: thm list -> int -> tactic
   val forward_tac: Proof.context -> thm list -> int -> tactic
   val dresolve0_tac: thm list -> int -> tactic
   val dresolve_tac: Proof.context -> thm list -> int -> tactic
   val atac: int -> tactic
   val rtac: thm -> int -> tactic
   val dtac: thm -> int -> tactic
   val etac: thm -> int -> tactic
-  val ftac: thm -> int -> tactic
   val ares_tac: Proof.context -> thm list -> int -> tactic
   val solve_tac: Proof.context -> thm list -> int -> tactic
   val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
   val match_tac: Proof.context -> thm list -> int -> tactic
   val ematch_tac: Proof.context -> thm list -> int -> tactic

 (*Resolution with elimination rules only*)
 fun eresolve0_tac rules = biresolve0_tac (map (pair true) rules);
 fun eresolve_tac ctxt rules = biresolve_tac ctxt (map (pair true) rules);
 
 (*Forward reasoning using destruction rules.*)
-fun forward0_tac rls = resolve0_tac (map make_elim rls) THEN' atac;
 fun forward_tac ctxt rls = resolve_tac ctxt (map make_elim rls) THEN' atac;
 
 (*Like forward_tac, but deletes the assumption after use.*)
 fun dresolve0_tac rls = eresolve0_tac (map make_elim rls);
 fun dresolve_tac ctxt rls = eresolve_tac ctxt (map make_elim rls);
 
 (*Shorthand versions: for resolution with a single theorem*)
 fun rtac rl =  resolve0_tac [rl];
 fun dtac rl = dresolve0_tac [rl];
 fun etac rl = eresolve0_tac [rl];
-fun ftac rl =  forward0_tac [rl];
 
 (*Use an assumption or some rules*)
 fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules;
 
 fun solve_tac ctxt rules = resolve_tac ctxt rules THEN_ALL_NEW assume_tac ctxt;