--- a/NEWS Fri Oct 23 10:11:56 2009 +0200
+++ b/NEWS Fri Oct 23 17:12:36 2009 +0200
@@ -165,7 +165,8 @@
* New implementation of quickcheck uses generic code generator;
default generators are provided for all suitable HOL types, records
-and datatypes.
+and datatypes. Old quickcheck can be re-activated importing
+theory Library/SML_Quickcheck.
* Renamed theorems:
Suc_eq_add_numeral_1 -> Suc_eq_plus1
--- a/src/HOL/HOL.thy Fri Oct 23 10:11:56 2009 +0200
+++ b/src/HOL/HOL.thy Fri Oct 23 17:12:36 2009 +0200
@@ -2002,8 +2002,12 @@
*} "solve goal by normalization"
+subsection {* Counterexample Search Units *}
+
subsubsection {* Quickcheck *}
+quickcheck_params [size = 5, iterations = 50]
+
ML {*
structure Quickcheck_RecFun_Simps = Named_Thms
(
@@ -2014,37 +2018,8 @@
setup Quickcheck_RecFun_Simps.setup
-setup {*
- Quickcheck.add_generator ("SML", Codegen.test_term)
-*}
-quickcheck_params [size = 5, iterations = 50]
-
-subsection {* Preprocessing for the predicate compiler *}
-
-ML {*
-structure Predicate_Compile_Alternative_Defs = Named_Thms
-(
- val name = "code_pred_def"
- val description = "alternative definitions of constants for the Predicate Compiler"
-)
-*}
-
-ML {*
-structure Predicate_Compile_Inline_Defs = Named_Thms
-(
- val name = "code_pred_inline"
- val description = "inlining definitions for the Predicate Compiler"
-)
-*}
-
-setup {*
- Predicate_Compile_Alternative_Defs.setup
- #> Predicate_Compile_Inline_Defs.setup
- #> Predicate_Compile_Preproc_Const_Defs.setup
-*}
-
-subsection {* Nitpick setup *}
+subsubsection {* Nitpick setup *}
text {* This will be relocated once Nitpick is moved to HOL. *}
@@ -2079,6 +2054,31 @@
*}
+subsection {* Preprocessing for the predicate compiler *}
+
+ML {*
+structure Predicate_Compile_Alternative_Defs = Named_Thms
+(
+ val name = "code_pred_def"
+ val description = "alternative definitions of constants for the Predicate Compiler"
+)
+*}
+
+ML {*
+structure Predicate_Compile_Inline_Defs = Named_Thms
+(
+ val name = "code_pred_inline"
+ val description = "inlining definitions for the Predicate Compiler"
+)
+*}
+
+setup {*
+ Predicate_Compile_Alternative_Defs.setup
+ #> Predicate_Compile_Inline_Defs.setup
+ #> Predicate_Compile_Preproc_Const_Defs.setup
+*}
+
+
subsection {* Legacy tactics and ML bindings *}
ML {*
--- a/src/HOL/IsaMakefile Fri Oct 23 10:11:56 2009 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 23 17:12:36 2009 +0200
@@ -358,7 +358,7 @@
Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML \
$(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML \
Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy \
- Library/OptionalSugar.thy
+ Library/OptionalSugar.thy Library/SML_Quickcheck.thy
@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
--- a/src/HOL/Library/Library.thy Fri Oct 23 10:11:56 2009 +0200
+++ b/src/HOL/Library/Library.thy Fri Oct 23 17:12:36 2009 +0200
@@ -52,6 +52,7 @@
Ramsey
Reflection
RBT
+ SML_Quickcheck
State_Monad
Sum_Of_Squares
Topology_Euclidean_Space
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/SML_Quickcheck.thy Fri Oct 23 17:12:36 2009 +0200
@@ -0,0 +1,12 @@
+
+header {* Install quickcheck of SML code generator *}
+
+theory SML_Quickcheck
+imports Main
+begin
+
+setup {*
+ Quickcheck.add_generator ("SML", Codegen.test_term)
+*}
+
+end