src/FOLP/classical.ML

   val rep_claset: claset -> 
       {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, 
        safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
        haz_brls: (bool*thm)list}
   val best_tac : claset -> int -> tactic
-  val chain_tac : int -> tactic
   val contr_tac : int -> tactic
   val fast_tac : claset -> int -> tactic
   val inst_step_tac : int -> tactic
   val joinrules : thm list * thm list -> (bool * thm) list
   val mp_tac: int -> tactic

 fun swap_res_tac rls = 
     let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap))
     in  assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls)
     end;
 
-(*Given assumption P-->Q, reduces subgoal Q to P [deletes the implication!] *)
-fun chain_tac i =
-    eresolve_tac [imp_elim] i  THEN
-    (assume_tac (i+1)  ORELSE  contr_tac (i+1));
 
 (*** Classical rule sets ***)
 
 datatype claset =
  CS of {safeIs: thm list,