| changeset 16955 | 93270c5f56f6 |
| parent 16925 | 0fd7b1438d28 |
| child 17091 | 13593aa6a546 |
--- 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 *)