src/HOL/Quickcheck_Narrowing.thy
changeset 43702 24fb44c1086a
parent 43562 2c55eac2e5a9
child 43887 442aceb54969
--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 08 13:59:54 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 08 14:37:19 2011 +0200
@@ -5,9 +5,9 @@
 theory Quickcheck_Narrowing
 imports Quickcheck_Exhaustive
 uses
-  ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
-  ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
-  ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
+  ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
+  ("Tools/Quickcheck/Narrowing_Engine.hs")
+  ("Tools/Quickcheck/narrowing_generators.ML")
 begin
 
 subsection {* Counterexample generator *}
@@ -352,9 +352,7 @@
 
 subsubsection {* Setting up the counterexample generator *}
 
-setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")) *}
-setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")) *}
-use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
+use "Tools/Quickcheck/narrowing_generators.ML"
 
 setup {* Narrowing_Generators.setup *}