| changeset 48891 | c0eafbd55de3 |
| parent 48375 | 48628962976b |
| child 51645 | 86e8c87e1f1b |
--- a/src/HOL/TPTP/ATP_Theory_Export.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory ATP_Theory_Export imports Complex_Main -uses "atp_theory_export.ML" begin +ML_file "atp_theory_export.ML" + ML {* open ATP_Problem open ATP_Theory_Export