chain_tac: deleted; just use etac mp
authorlcp
Tue Jul 12 18:30:53 1994 +0200 (1994-07-12)
changeset 469b571d997178d
parent 468 3dd1dcb509ac
child 470 6cb6dd05d761
chain_tac: deleted; just use etac mp
src/FOLP/classical.ML
src/Provers/classical.ML
     1.1 --- a/src/FOLP/classical.ML	Tue Jul 12 18:20:39 1994 +0200
     1.2 +++ b/src/FOLP/classical.ML	Tue Jul 12 18:30:53 1994 +0200
     1.3 @@ -46,7 +46,6 @@
     1.4         safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
     1.5         haz_brls: (bool*thm)list}
     1.6    val best_tac : claset -> int -> tactic
     1.7 -  val chain_tac : int -> tactic
     1.8    val contr_tac : int -> tactic
     1.9    val fast_tac : claset -> int -> tactic
    1.10    val inst_step_tac : int -> tactic
    1.11 @@ -90,10 +89,6 @@
    1.12      in  assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls)
    1.13      end;
    1.14  
    1.15 -(*Given assumption P-->Q, reduces subgoal Q to P [deletes the implication!] *)
    1.16 -fun chain_tac i =
    1.17 -    eresolve_tac [imp_elim] i  THEN
    1.18 -    (assume_tac (i+1)  ORELSE  contr_tac (i+1));
    1.19  
    1.20  (*** Classical rule sets ***)
    1.21  
     2.1 --- a/src/Provers/classical.ML	Tue Jul 12 18:20:39 1994 +0200
     2.2 +++ b/src/Provers/classical.ML	Tue Jul 12 18:30:53 1994 +0200
     2.3 @@ -41,7 +41,6 @@
     2.4    val rep_claset: claset -> 
     2.5        {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list}
     2.6    val best_tac : claset -> int -> tactic
     2.7 -  val chain_tac : int -> tactic
     2.8    val contr_tac : int -> tactic
     2.9    val eq_mp_tac: int -> tactic
    2.10    val fast_tac : claset -> int -> tactic
    2.11 @@ -89,10 +88,6 @@
    2.12          biresolve_tac (foldr addrl (rls,[]))
    2.13      end;
    2.14  
    2.15 -(*Given assumption P-->Q, reduces subgoal Q to P [deletes the implication!] *)
    2.16 -fun chain_tac i =
    2.17 -    eresolve_tac [imp_elim] i  THEN
    2.18 -    (assume_tac (i+1)  ORELSE  contr_tac (i+1));
    2.19  
    2.20  (*** Classical rule sets ***)
    2.21