adding narrowing instance for sets
authorbulwahn
Fri, 20 Jan 2012 09:28:53 +0100
changeset 46308 e5abbec2697a
parent 46307 ec8f975c059b
child 46309 693d8d7bc3cd
adding narrowing instance for sets
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 *}