changeset 49985 | 5b4b0e4e5205 |
parent 48891 | c0eafbd55de3 |
child 52470 | dedd7952a62c |
--- a/src/HOL/TPTP/ATP_Problem_Import.thy Wed Oct 31 11:23:21 2012 +0100 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Wed Oct 31 11:23:21 2012 +0100 @@ -5,7 +5,10 @@ header {* ATP Problem Importer *} theory ATP_Problem_Import -imports Complex_Main TPTP_Interpret +imports + Complex_Main + TPTP_Interpret + "~~/src/HOL/Library/Refute" begin ML_file "sledgehammer_tactics.ML"