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