# HG changeset patch
# User bulwahn
# Date 1307601136 -7200
# Node ID 1efdcb579b6cc2e2446d4b62c4f601ba57469362
# Parent  d1265a4d8ae1f74be9f23923e9a696c3aa5a9b42
adding theory Quickcheck_Narrowing to HOL-Main image

diff -r d1265a4d8ae1 -r 1efdcb579b6c src/HOL/Record.thy
--- a/src/HOL/Record.thy	Thu Jun 09 08:32:15 2011 +0200
+++ b/src/HOL/Record.thy	Thu Jun 09 08:32:16 2011 +0200
@@ -9,7 +9,7 @@
 header {* Extensible records with structural subtyping *}
 
 theory Record
-imports Plain Quickcheck_Exhaustive
+imports Plain Quickcheck_Narrowing
 uses ("Tools/record.ML")
 begin