src/HOL/Tools/res_atp.ML
changeset 16955 93270c5f56f6
parent 16925 0fd7b1438d28
child 17091 13593aa6a546
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jul 28 17:54:39 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jul 28 17:55:39 2005 +0200
     1.3 @@ -73,11 +73,6 @@
     1.4      String.translate (fn c => if is_proof_char c then str c else "");
     1.5  
     1.6  
     1.7 -(*
     1.8 -fun call_atp_tac thms n = (tptp_inputs thms ; dummy_tac);
     1.9 -
    1.10 -*)
    1.11 -
    1.12  (**** For running in Isar ****)
    1.13  
    1.14  (* same function as that in res_axioms.ML *)