--- 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 ***)
--- a/src/Provers/classical.ML Tue Jul 12 18:20:39 1994 +0200
+++ b/src/Provers/classical.ML Tue Jul 12 18:30:53 1994 +0200
@@ -41,7 +41,6 @@
val rep_claset: claset ->
{safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list}
val best_tac : claset -> int -> tactic
- val chain_tac : int -> tactic
val contr_tac : int -> tactic
val eq_mp_tac: int -> tactic
val fast_tac : claset -> int -> tactic
@@ -89,10 +88,6 @@
biresolve_tac (foldr addrl (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 ***)