| changeset 47766 | 9f7cdd5fff7c |
| parent 47765 | 18f37b7aa6a6 |
| child 47770 | 53e30966b4b6 |
--- a/src/HOL/TPTP/ATP_Problem_Import.thy Wed Apr 25 22:00:33 2012 +0200 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Wed Apr 25 22:00:33 2012 +0200 @@ -6,7 +6,8 @@ theory ATP_Problem_Import imports Complex_Main TPTP_Interpret -uses ("atp_problem_import.ML") +uses "~~/src/HOL/ex/sledgehammer_tactics.ML" + ("atp_problem_import.ML") begin ML {* Proofterm.proofs := 0 *}