chain_tac: deleted; just use etac mp
authorlcp
Tue, 12 Jul 1994 18:30:53 +0200
changeset 469 b571d997178d
parent 468 3dd1dcb509ac
child 470 6cb6dd05d761
chain_tac: deleted; just use etac mp
src/FOLP/classical.ML
src/Provers/classical.ML
--- 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 ***)