--- a/src/HOL/Main.thy Tue Mar 11 17:18:39 2014 +0100
+++ b/src/HOL/Main.thy Tue Mar 11 17:18:41 2014 +0100
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Predicate_Compile Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
+imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
begin
text {*
--- a/src/HOL/Record.thy Tue Mar 11 17:18:39 2014 +0100
+++ b/src/HOL/Record.thy Tue Mar 11 17:18:41 2014 +0100
@@ -9,7 +9,7 @@
header {* Extensible records with structural subtyping *}
theory Record
-imports Quickcheck_Exhaustive Quickcheck_Narrowing
+imports Quickcheck_Exhaustive
keywords "record" :: thy_decl
begin