# HG changeset patch
# User bulwahn
# Date 1299853273 -3600
# Node ID fc070c5f3a4cad1c8a3d49c5564c5b9d0014173a
# Parent  ee84fc7a61f122adf624af0227a509878ef5e6be
adapting Quickcheck theory after moving ML files

diff -r ee84fc7a61f1 -r fc070c5f3a4c src/HOL/Quickcheck.thy
--- 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
@@ -1,10 +1,10 @@
-(* Author: Florian Haftmann, TU Muenchen *)
+(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
 
-header {* A simple counterexample generator *}
+header {* A simple counterexample generator performing random testing *}
 
 theory Quickcheck
 imports Random Code_Evaluation Enum
-uses ("Tools/quickcheck_generators.ML")
+uses ("Tools/Quickcheck/random_generators.ML")
 begin
 
 notation fcomp (infixl "\<circ>>" 60)
@@ -126,7 +126,7 @@
   shows "random_aux k = rhs k"
   using assms by (rule code_numeral.induct)
 
-use "Tools/quickcheck_generators.ML"
+use "Tools/Quickcheck/random_generators.ML"
 setup Quickcheck_Generators.setup