src/HOL/TPTP/ATP_Problem_Import.thy
changeset 49985 5b4b0e4e5205
parent 48891 c0eafbd55de3
child 52470 dedd7952a62c
     1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Oct 31 11:23:21 2012 +0100
     1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Oct 31 11:23:21 2012 +0100
     1.3 @@ -5,7 +5,10 @@
     1.4  header {* ATP Problem Importer *}
     1.5  
     1.6  theory ATP_Problem_Import
     1.7 -imports Complex_Main TPTP_Interpret
     1.8 +imports
     1.9 +  Complex_Main
    1.10 +  TPTP_Interpret
    1.11 +  "~~/src/HOL/Library/Refute"
    1.12  begin
    1.13  
    1.14  ML_file "sledgehammer_tactics.ML"