src/HOL/TPTP/ATP_Problem_Import.thy
changeset 47770 53e30966b4b6
parent 47766 9f7cdd5fff7c
child 47785 d27bb852c430
     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 23:39:19 2012 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  theory ATP_Problem_Import
     1.5  imports Complex_Main TPTP_Interpret
     1.6  uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
     1.7 -     ("atp_problem_import.ML")
     1.8 +     "atp_problem_import.ML"
     1.9  begin
    1.10  
    1.11  ML {* Proofterm.proofs := 0 *}
    1.12 @@ -15,6 +15,4 @@
    1.13  declare [[show_consts]] (* for Refute *)
    1.14  declare [[smt_oracle]]
    1.15  
    1.16 -use "atp_problem_import.ML"
    1.17 -
    1.18  end