changeset 47790 | 2e1636e45770 |
parent 47687 | bfbd2d0bb348 |
child 48891 | c0eafbd55de3 |
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy Fri Apr 27 14:07:31 2012 +0200 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Fri Apr 27 15:24:37 2012 +0200 @@ -6,7 +6,7 @@ theory TPTP_Parser_Example imports TPTP_Parser TPTP_Interpret -uses "~~/src/HOL/ex/sledgehammer_tactics.ML" +uses "sledgehammer_tactics.ML" begin import_tptp "$TPTP/Problems/CSR/CSR077+1.p"