src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy
changeset 58813 625d04d4fd2a
parent 58148 9764b994a421
child 63167 0909deb8059b
equal deleted inserted replaced
58812:5a9a2d3b9f8b 58813:625d04d4fd2a
     9 text {*
     9 text {*
    10 
    10 
    11 First, this requires to setup special generators for all datatypes via the following command.
    11 First, this requires to setup special generators for all datatypes via the following command.
    12 *}
    12 *}
    13 
    13 
    14 setup {* Exhaustive_Generators.setup_bounded_forall_datatype_interpretation *}
    14 setup Exhaustive_Generators.setup_bounded_forall_datatype_interpretation
    15 
    15 
    16 text {*
    16 text {*
    17 Now, the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
    17 Now, the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
    18 takes formulas of type bool with free variables, and returns a list of testing functions.
    18 takes formulas of type bool with free variables, and returns a list of testing functions.
    19 *}
    19 *}