# HG changeset patch # User bulwahn # Date 1341222319 -7200 # Node ID 0192811f0a961ece1b2ef8cbc05764716d33b88b # Parent eb72f99737be80d7f94a5f28034fba7541539222 exporting important function for the "many conjecture refutation" compilation of quickcheck diff -r eb72f99737be -r 0192811f0a96 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 02 11:39:24 2012 +0200 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 02 11:45:19 2012 +0200 @@ -20,6 +20,7 @@ val optimise_equality : bool Config.T val quickcheck_pretty : bool Config.T val setup_exhaustive_datatype_interpretation : theory -> theory + val setup_bounded_forall_datatype_interpretation : theory -> theory val setup: theory -> theory val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr -> @@ -564,6 +565,11 @@ val setup_exhaustive_datatype_interpretation = Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype) +val setup_bounded_forall_datatype_interpretation = + Datatype.interpretation (Quickcheck_Common.ensure_sort + (((@{sort type}, @{sort type}), @{sort bounded_forall}), + (Datatype.the_descr, instantiate_bounded_forall_datatype))) + val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true); val setup =