changeset 48891 | c0eafbd55de3 |
parent 47790 | 2e1636e45770 |
child 53393 | 5278312037f8 |
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory TPTP_Parser_Example imports TPTP_Parser TPTP_Interpret -uses "sledgehammer_tactics.ML" begin +ML_file "sledgehammer_tactics.ML" + import_tptp "$TPTP/Problems/CSR/CSR077+1.p" ML {*