# HG changeset patch
# User blanchet
# Date 1394554719 -3600
# Node ID 1f283d0a4966a414c8f5915ddd1f55436250c64b
# Parent  683148f3ae48aa23da60c7461bb7be78527fe119
make it possible to load Quickcheck exhaustive & narrowing in parallel

diff -r 683148f3ae48 -r 1f283d0a4966 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Tue Mar 11 15:34:38 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Tue Mar 11 17:18:39 2014 +0100
@@ -3,7 +3,7 @@
 header {* Counterexample generator performing narrowing-based testing *}
 
 theory Quickcheck_Narrowing
-imports Quickcheck_Exhaustive
+imports Quickcheck_Random
 keywords "find_unused_assms" :: diag
 begin
 
diff -r 683148f3ae48 -r 1f283d0a4966 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Tue Mar 11 15:34:38 2014 +0100
+++ b/src/HOL/Record.thy	Tue Mar 11 17:18:39 2014 +0100
@@ -9,7 +9,7 @@
 header {* Extensible records with structural subtyping *}
 
 theory Record
-imports Quickcheck_Narrowing
+imports Quickcheck_Exhaustive Quickcheck_Narrowing
 keywords "record" :: thy_decl
 begin