exporting instantiation functions in quickcheck for their usage in abstract generators
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Dec 20 17:22:31 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Dec 20 17:22:31 2011 +0100
@@ -20,6 +20,9 @@
val quickcheck_pretty : bool Config.T
val setup_exhaustive_datatype_interpretation : theory -> theory
val setup: theory -> theory
+
+ val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
+ (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
end;
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =