src/HOL/TPTP/TPTP_Parser_Example.thy
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"