author | paulson |
Thu, 28 Jul 2005 17:55:39 +0200 | |
changeset 16955 | 93270c5f56f6 |
parent 16954 | 82d0a25c5a1d |
child 16956 | 5b413c866593 |
--- a/src/HOL/Tools/res_atp.ML Thu Jul 28 17:54:39 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Jul 28 17:55:39 2005 +0200 @@ -73,11 +73,6 @@ String.translate (fn c => if is_proof_char c then str c else ""); -(* -fun call_atp_tac thms n = (tptp_inputs thms ; dummy_tac); - -*) - (**** For running in Isar ****) (* same function as that in res_axioms.ML *)