Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
exporting instantiation functions in quickcheck for their usage in abstract generators
authorbulwahn
Tue, 20 Dec 2011 17:22:31 +0100
changeset 45924 f03dd48829d8
parent 45923 473b744c23f2
child 45925 cd4243c025bb
exporting instantiation functions in quickcheck for their usage in abstract generators
src/HOL/Tools/Quickcheck/exhaustive_generators.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle