deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
authorbulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 4231612635bb655fd
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
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
     1.1 --- a/src/HOL/Library/Code_Char.thy	Fri Apr 08 16:31:14 2011 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Fri Apr 08 16:31:14 2011 +0200
     1.3 @@ -59,6 +59,6 @@
     1.4    (Scala "!(_.toList)")
     1.5  
     1.6  
     1.7 -declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]
     1.8 +(*declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]*)
     1.9  
    1.10  end
     2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
     2.3 @@ -533,13 +533,13 @@
     2.4  
     2.5  val setup =
     2.6    Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     2.7 +      (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
     2.8 +(* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     2.9        (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
    2.10    #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.11 -      (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
    2.12 -  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.13        (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
    2.14    #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.15 -      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
    2.16 +      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
    2.17    #> setup_smart_quantifier
    2.18    #> setup_full_support
    2.19    #> setup_fast