src/HOL/Quickcheck.thy
changeset 41922 fc070c5f3a4c
parent 40973 890fefa597af
child 41923 f05fc0711bc7
     1.1 --- a/src/HOL/Quickcheck.thy	Fri Mar 11 15:21:13 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck.thy	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -1,10 +1,10 @@
     1.4 -(* Author: Florian Haftmann, TU Muenchen *)
     1.5 +(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
     1.6  
     1.7 -header {* A simple counterexample generator *}
     1.8 +header {* A simple counterexample generator performing random testing *}
     1.9  
    1.10  theory Quickcheck
    1.11  imports Random Code_Evaluation Enum
    1.12 -uses ("Tools/quickcheck_generators.ML")
    1.13 +uses ("Tools/Quickcheck/random_generators.ML")
    1.14  begin
    1.15  
    1.16  notation fcomp (infixl "\<circ>>" 60)
    1.17 @@ -126,7 +126,7 @@
    1.18    shows "random_aux k = rhs k"
    1.19    using assms by (rule code_numeral.induct)
    1.20  
    1.21 -use "Tools/quickcheck_generators.ML"
    1.22 +use "Tools/Quickcheck/random_generators.ML"
    1.23  setup Quickcheck_Generators.setup
    1.24  
    1.25