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.
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
authorbulwahn
Fri, 08 Apr 2011 16:31:14 +0200
changeset 42316 12635bb655fd
parent 42315 95dfa082065a
child 42317 c2b5dbb76b7e
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
src/HOL/Library/Code_Char.thy file | annotate | diff | comparison | revisions
src/HOL/Tools/Quickcheck/exhaustive_generators.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Code_Char.thy	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/Library/Code_Char.thy	Fri Apr 08 16:31:14 2011 +0200
@@ -59,6 +59,6 @@
   (Scala "!(_.toList)")
 
 
-declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]
+(*declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]*)
 
 end
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
@@ -533,13 +533,13 @@
 
 val setup =
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+      (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
+(* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
-      (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
-  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
-      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
+      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
   #> setup_smart_quantifier
   #> setup_full_support
   #> setup_fast
isabelle