tuned order
authorhaftmann
Wed Jun 10 16:10:30 2009 +0200 (2009-06-10)
changeset 31607674348914ebc
parent 31606 f896c4cce1eb
child 31608 a98a47ffdd8d
tuned order
src/HOL/Quickcheck.thy
     1.1 --- a/src/HOL/Quickcheck.thy	Wed Jun 10 15:05:38 2009 +0200
     1.2 +++ b/src/HOL/Quickcheck.thy	Wed Jun 10 16:10:30 2009 +0200
     1.3 @@ -129,13 +129,13 @@
     1.4  use "Tools/quickcheck_generators.ML"
     1.5  setup {* Quickcheck_Generators.setup *}
     1.6  
     1.7 -code_reserved Quickcheck Quickcheck_Generators
     1.8 -
     1.9  code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
    1.10    -- {* With enough criminal energy this can be abused to derive @{prop False};
    1.11    for this reason we use a distinguished target @{text Quickcheck}
    1.12    not spoiling the regular trusted code generation *}
    1.13  
    1.14 +code_reserved Quickcheck Quickcheck_Generators
    1.15 +
    1.16  
    1.17  hide (open) const collapse beyond random_fun_aux random_fun_lift
    1.18