src/HOL/TPTP/ATP_Problem_Import.thy
changeset 57812 8dc9dc241973
parent 52487 48bc24467008
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Thu Aug 07 12:17:41 2014 +0200
     1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Thu Aug 07 12:17:41 2014 +0200
     1.3 @@ -5,10 +5,7 @@
     1.4  header {* ATP Problem Importer *}
     1.5  
     1.6  theory ATP_Problem_Import
     1.7 -imports
     1.8 -  Complex_Main
     1.9 -  TPTP_Interpret
    1.10 -  "~~/src/HOL/Library/Refute"
    1.11 +imports Complex_Main TPTP_Interpret "~~/src/HOL/Library/Refute"
    1.12  begin
    1.13  
    1.14  ML_file "sledgehammer_tactics.ML"
    1.15 @@ -24,8 +21,7 @@
    1.16  ML_file "atp_problem_import.ML"
    1.17  
    1.18  (*
    1.19 -ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50
    1.20 -          "$TPTP/Problems/PUZ/PUZ107^5.p" *}
    1.21 +ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
    1.22  *)
    1.23  
    1.24  end