--- a/src/HOL/TPTP/ATP_Problem_Import.thy Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Thu Aug 07 12:17:41 2014 +0200
@@ -5,10 +5,7 @@
header {* ATP Problem Importer *}
theory ATP_Problem_Import
-imports
- Complex_Main
- TPTP_Interpret
- "~~/src/HOL/Library/Refute"
+imports Complex_Main TPTP_Interpret "~~/src/HOL/Library/Refute"
begin
ML_file "sledgehammer_tactics.ML"
@@ -24,8 +21,7 @@
ML_file "atp_problem_import.ML"
(*
-ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50
- "$TPTP/Problems/PUZ/PUZ107^5.p" *}
+ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
*)
end