src/HOL/Quickcheck_Narrowing.thy
changeset 43702 24fb44c1086a
parent 43562 2c55eac2e5a9
child 43887 442aceb54969
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 08 13:59:54 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 08 14:37:19 2011 +0200
     1.3 @@ -5,9 +5,9 @@
     1.4  theory Quickcheck_Narrowing
     1.5  imports Quickcheck_Exhaustive
     1.6  uses
     1.7 -  ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
     1.8 -  ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
     1.9 -  ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
    1.10 +  ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
    1.11 +  ("Tools/Quickcheck/Narrowing_Engine.hs")
    1.12 +  ("Tools/Quickcheck/narrowing_generators.ML")
    1.13  begin
    1.14  
    1.15  subsection {* Counterexample generator *}
    1.16 @@ -352,9 +352,7 @@
    1.17  
    1.18  subsubsection {* Setting up the counterexample generator *}
    1.19  
    1.20 -setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")) *}
    1.21 -setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")) *}
    1.22 -use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
    1.23 +use "Tools/Quickcheck/narrowing_generators.ML"
    1.24  
    1.25  setup {* Narrowing_Generators.setup *}
    1.26