--- a/src/FOLP/classical.ML Tue Jul 12 18:20:39 1994 +0200
+++ b/src/FOLP/classical.ML Tue Jul 12 18:30:53 1994 +0200
@@ -46,7 +46,6 @@
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
@@ -90,10 +89,6 @@
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 ***)