# HG changeset patch
# User haftmann
# Date 1256310756 -7200
# Node ID cd1579e0997a4b0ad1e5cb57564936445543b2b8
# Parent  fe29679cabc23a34bebb7e8ca6a25928d7720260
turned off old quickcheck

diff -r fe29679cabc2 -r cd1579e0997a NEWS
--- 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
diff -r fe29679cabc2 -r cd1579e0997a src/HOL/HOL.thy
--- 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 {*
diff -r fe29679cabc2 -r cd1579e0997a src/HOL/IsaMakefile
--- 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
 
 
diff -r fe29679cabc2 -r cd1579e0997a src/HOL/Library/Library.thy
--- 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
diff -r fe29679cabc2 -r cd1579e0997a src/HOL/Library/SML_Quickcheck.thy
--- /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