adapting Quickcheck theory after moving ML files
authorbulwahn
Fri, 11 Mar 2011 15:21:13 +0100
changeset 41922 fc070c5f3a4c
parent 41921 ee84fc7a61f1
child 41923 f05fc0711bc7
adapting Quickcheck theory after moving ML files
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