make it possible to load Quickcheck exhaustive & narrowing in parallel
authorblanchet
Tue, 11 Mar 2014 17:18:39 +0100
changeset 56047 1f283d0a4966
parent 56046 683148f3ae48
child 56048 d311c6377e08
make it possible to load Quickcheck exhaustive & narrowing in parallel
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Record.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
 
--- 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