src/HOL/Quickcheck_Narrowing.thy

--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jan 20 09:28:52 2012 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jan 20 09:28:53 2012 +0100
@@ -367,6 +367,16 @@
       z = (conv :: _ => _ => unit)  in f)"
 unfolding Let_def ensure_testable_def ..
 
+subsection {* Narrowing for sets *}
+
+instantiation set :: (narrowing) narrowing
+begin
+
+definition "narrowing_set = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons set) narrowing"
+
+instance ..
+
+end
   
 subsection {* Narrowing for integers *}