--- a/src/HOL/Quickcheck.thy Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Quickcheck.thy Fri Mar 11 15:21:13 2011 +0100
@@ -127,7 +127,7 @@
using assms by (rule code_numeral.induct)
use "Tools/Quickcheck/random_generators.ML"
-setup Quickcheck_Generators.setup
+setup Random_Generators.setup
subsection {* Code setup *}
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 11 15:21:13 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/exhaustive_generators.ML
+(* Title: HOL/Tools/Quickcheck/exhaustive_generators.ML
Author: Lukas Bulwahn, TU Muenchen
Exhaustive generators for various types.
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 11 15:21:13 2011 +0100
@@ -1,10 +1,10 @@
-(* Title: HOL/Tools/quickcheck_generators.ML
+(* Title: HOL/Tools/Quickcheck/random_generators.ML
Author: Florian Haftmann, TU Muenchen
-Quickcheck generators for various types.
+Random generators for various types.
*)
-signature QUICKCHECK_GENERATORS =
+signature RANDOM_GENERATORS =
sig
type seed = Random_Engine.seed
val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
@@ -25,7 +25,7 @@
val setup: theory -> theory
end;
-structure Quickcheck_Generators : QUICKCHECK_GENERATORS =
+structure Random_Generators : RANDOM_GENERATORS =
struct
(** abstract syntax **)
@@ -424,7 +424,7 @@
let
val t' = mk_reporting_generator_expr thy t Ts;
val compile = Code_Runtime.dynamic_value_strict
- (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
+ (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
val single_tester = compile #> Random_Engine.run
fun iterate_and_collect size 0 report = (NONE, report)
@@ -445,7 +445,7 @@
let
val t' = mk_generator_expr thy t Ts;
val compile = Code_Runtime.dynamic_value_strict
- (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
+ (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
val single_tester = compile #> Random_Engine.run
fun iterate size 0 = NONE