src/HOL/Quickcheck_Exhaustive.thy
changeset 45925 cd4243c025bb
parent 45818 53a697f5454a
child 46193 55a4769d0abe
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Tue Dec 20 17:22:31 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Dec 20 17:39:56 2011 +0100
     1.3 @@ -4,7 +4,9 @@
     1.4  
     1.5  theory Quickcheck_Exhaustive
     1.6  imports Quickcheck
     1.7 -uses ("Tools/Quickcheck/exhaustive_generators.ML")
     1.8 +uses
     1.9 +  ("Tools/Quickcheck/exhaustive_generators.ML")
    1.10 +  ("Tools/Quickcheck/abstract_generators.ML")
    1.11  begin
    1.12  
    1.13  subsection {* basic operations for exhaustive generators *}
    1.14 @@ -521,7 +523,7 @@
    1.15  where
    1.16    "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
    1.17  
    1.18 -subsection {* Defining combinators for any first-order data type *}
    1.19 +subsection {* Defining generators for any first-order data type *}
    1.20  
    1.21  axiomatization unknown :: 'a
    1.22  
    1.23 @@ -533,6 +535,10 @@
    1.24  
    1.25  declare [[quickcheck_batch_tester = exhaustive]]
    1.26  
    1.27 +subsection {* Defining generators for abstract types *}
    1.28 +
    1.29 +use "Tools/Quickcheck/abstract_generators.ML"
    1.30 +
    1.31  hide_fact orelse_def
    1.32  no_notation orelse (infixr "orelse" 55)
    1.33