author | bulwahn |
Fri, 20 Jan 2012 09:28:53 +0100 | |
changeset 46308 | e5abbec2697a |
parent 46307 | ec8f975c059b |
child 46309 | 693d8d7bc3cd |
--- 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 *}