# HG changeset patch
# User bulwahn
# Date 1327048133 -3600
# Node ID e5abbec2697a5acdbb5b5ed28f9bd711f2c2be33
# Parent  ec8f975c059b206206c0e4a14bd10d13162aedfc
adding narrowing instance for sets

diff -r ec8f975c059b -r e5abbec2697a 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 *}