src/FOLP/classical.ML
changeset 469 b571d997178d
parent 0 a5a9c433f639
child 1459 d12da312eff4
     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