| changeset 72001 | 3e08311ada8e |
| parent 69605 | a96320074298 |
| child 73684 | a63d76ba0a03 |
--- a/src/HOL/TPTP/ATP_Problem_Import.thy Mon Jul 06 10:47:30 2020 +0000 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Mon Jul 06 16:52:48 2020 +0200 @@ -5,7 +5,7 @@ section \<open>ATP Problem Importer\<close> theory ATP_Problem_Import -imports Complex_Main TPTP_Interpret "HOL-Library.Refute" + imports Complex_Main TPTP_Interpret "HOL-Library.Refute" begin ML_file \<open>sledgehammer_tactics.ML\<close>