1.1 --- a/NEWS	Fri Oct 23 10:11:56 2009 +0200
     1.2 +++ b/NEWS	Fri Oct 23 17:12:36 2009 +0200
     1.3 @@ -165,7 +165,8 @@
     1.4  
     1.5  * New implementation of quickcheck uses generic code generator;
     1.6  default generators are provided for all suitable HOL types, records
     1.7 -and datatypes.
     1.8 +and datatypes.  Old quickcheck can be re-activated importing
     1.9 +theory Library/SML_Quickcheck.
    1.10  
    1.11  * Renamed theorems:
    1.12  Suc_eq_add_numeral_1 -> Suc_eq_plus1

     2.1 --- a/src/HOL/HOL.thy	Fri Oct 23 10:11:56 2009 +0200
     2.2 +++ b/src/HOL/HOL.thy	Fri Oct 23 17:12:36 2009 +0200
     2.3 @@ -2002,8 +2002,12 @@
     2.4  *} "solve goal by normalization"
     2.5  
     2.6  
     2.7 +subsection {* Counterexample Search Units *}
     2.8 +
     2.9  subsubsection {* Quickcheck *}
    2.10  
    2.11 +quickcheck_params [size = 5, iterations = 50]
    2.12 +
    2.13  ML {*
    2.14  structure Quickcheck_RecFun_Simps = Named_Thms
    2.15  (
    2.16 @@ -2014,37 +2018,8 @@
    2.17  
    2.18  setup Quickcheck_RecFun_Simps.setup
    2.19  
    2.20 -setup {*
    2.21 -  Quickcheck.add_generator ("SML", Codegen.test_term)
    2.22 -*}
    2.23  
    2.24 -quickcheck_params [size = 5, iterations = 50]
    2.25 -
    2.26 -subsection {* Preprocessing for the predicate compiler *}
    2.27 -
    2.28 -ML {*
    2.29 -structure Predicate_Compile_Alternative_Defs = Named_Thms
    2.30 -(
    2.31 -  val name = "code_pred_def"
    2.32 -  val description = "alternative definitions of constants for the Predicate Compiler"
    2.33 -)
    2.34 -*}
    2.35 -
    2.36 -ML {*
    2.37 -structure Predicate_Compile_Inline_Defs = Named_Thms
    2.38 -(
    2.39 -  val name = "code_pred_inline"
    2.40 -  val description = "inlining definitions for the Predicate Compiler"
    2.41 -)
    2.42 -*}
    2.43 -
    2.44 -setup {*
    2.45 -  Predicate_Compile_Alternative_Defs.setup
    2.46 -  #> Predicate_Compile_Inline_Defs.setup
    2.47 -  #> Predicate_Compile_Preproc_Const_Defs.setup
    2.48 -*}
    2.49 -
    2.50 -subsection {* Nitpick setup *}
    2.51 +subsubsection {* Nitpick setup *}
    2.52  
    2.53  text {* This will be relocated once Nitpick is moved to HOL. *}
    2.54  
    2.55 @@ -2079,6 +2054,31 @@
    2.56  *}
    2.57  
    2.58  
    2.59 +subsection {* Preprocessing for the predicate compiler *}
    2.60 +
    2.61 +ML {*
    2.62 +structure Predicate_Compile_Alternative_Defs = Named_Thms
    2.63 +(
    2.64 +  val name = "code_pred_def"
    2.65 +  val description = "alternative definitions of constants for the Predicate Compiler"
    2.66 +)
    2.67 +*}
    2.68 +
    2.69 +ML {*
    2.70 +structure Predicate_Compile_Inline_Defs = Named_Thms
    2.71 +(
    2.72 +  val name = "code_pred_inline"
    2.73 +  val description = "inlining definitions for the Predicate Compiler"
    2.74 +)
    2.75 +*}
    2.76 +
    2.77 +setup {*
    2.78 +  Predicate_Compile_Alternative_Defs.setup
    2.79 +  #> Predicate_Compile_Inline_Defs.setup
    2.80 +  #> Predicate_Compile_Preproc_Const_Defs.setup
    2.81 +*}
    2.82 +
    2.83 +
    2.84  subsection {* Legacy tactics and ML bindings *}
    2.85  
    2.86  ML {*

     3.1 --- a/src/HOL/IsaMakefile	Fri Oct 23 10:11:56 2009 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Fri Oct 23 17:12:36 2009 +0200
     3.3 @@ -358,7 +358,7 @@
     3.4    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML		\
     3.5    $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML		\
     3.6    Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy	\
     3.7 -  Library/OptionalSugar.thy
     3.8 +  Library/OptionalSugar.thy Library/SML_Quickcheck.thy
     3.9  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    3.10  
    3.11  

     4.1 --- a/src/HOL/Library/Library.thy	Fri Oct 23 10:11:56 2009 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Fri Oct 23 17:12:36 2009 +0200
     4.3 @@ -52,6 +52,7 @@
     4.4    Ramsey
     4.5    Reflection
     4.6    RBT
     4.7 +  SML_Quickcheck
     4.8    State_Monad
     4.9    Sum_Of_Squares
    4.10    Topology_Euclidean_Space

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/SML_Quickcheck.thy	Fri Oct 23 17:12:36 2009 +0200
     5.3 @@ -0,0 +1,12 @@
     5.4 +
     5.5 +header {* Install quickcheck of SML code generator *}
     5.6 +
     5.7 +theory SML_Quickcheck
     5.8 +imports Main
     5.9 +begin
    5.10 +
    5.11 +setup {*
    5.12 +  Quickcheck.add_generator ("SML", Codegen.test_term)
    5.13 +*}
    5.14 +
    5.15 +end