src/HOL/Quickcheck_Narrowing.thy
changeset 46308 e5abbec2697a
parent 46032 0da934e135b0
child 46589 689311986778
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jan 20 09:28:52 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jan 20 09:28:53 2012 +0100
     1.3 @@ -367,6 +367,16 @@
     1.4        z = (conv :: _ => _ => unit)  in f)"
     1.5  unfolding Let_def ensure_testable_def ..
     1.6  
     1.7 +subsection {* Narrowing for sets *}
     1.8 +
     1.9 +instantiation set :: (narrowing) narrowing
    1.10 +begin
    1.11 +
    1.12 +definition "narrowing_set = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons set) narrowing"
    1.13 +
    1.14 +instance ..
    1.15 +
    1.16 +end
    1.17    
    1.18  subsection {* Narrowing for integers *}
    1.19