src/HOL/Quickcheck_Narrowing.thy
changeset 66758 9312ce5a938d
parent 66148 5e60c2d0a1f1
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Mon Oct 02 19:28:18 2017 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Oct 02 19:38:39 2017 +0200
     1.3 @@ -192,6 +192,8 @@
     1.4  
     1.5  subsubsection \<open>Setting up the counterexample generator\<close>
     1.6  
     1.7 +external_file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"
     1.8 +external_file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"
     1.9  ML_file "Tools/Quickcheck/narrowing_generators.ML"
    1.10  
    1.11  definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"