src/HOL/Tools/Quickcheck/exhaustive_generators.ML
changeset 45924 f03dd48829d8
parent 45923 473b744c23f2
child 46042 ab32a87ba01a
equal deleted inserted replaced
45923:473b744c23f2 45924:f03dd48829d8
    18   exception Counterexample of term list
    18   exception Counterexample of term list
    19   val smart_quantifier : bool Config.T
    19   val smart_quantifier : bool Config.T
    20   val quickcheck_pretty : bool Config.T
    20   val quickcheck_pretty : bool Config.T
    21   val setup_exhaustive_datatype_interpretation : theory -> theory
    21   val setup_exhaustive_datatype_interpretation : theory -> theory
    22   val setup: theory -> theory
    22   val setup: theory -> theory
       
    23   
       
    24   val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
       
    25     (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
    23 end;
    26 end;
    24 
    27 
    25 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
    28 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
    26 struct
    29 struct
    27 
    30