# HG changeset patch
# User haftmann
# Date 1264597372 -3600
# Node ID ceeffca32eb01189edb52390b25438cac1a4c373
# Parent  52f30b06938a3aee95acef75817ea2b8c469bbd5
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy

diff -r 52f30b06938a -r ceeffca32eb0 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Mon Jan 25 19:31:50 2010 +0100
+++ b/src/HOL/Quickcheck.thy	Wed Jan 27 14:02:52 2010 +0100
@@ -126,9 +126,24 @@
   shows "random_aux k = rhs k"
   using assms by (rule code_numeral.induct)
 
-setup {* Quickcheck.setup *}
+use "Tools/quickcheck_generators.ML"
+setup Quickcheck_Generators.setup
+
+
+subsection {* Code setup *}
 
-subsection {* the Random-Predicate Monad *} 
+code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
+  -- {* With enough criminal energy this can be abused to derive @{prop False};
+  for this reason we use a distinguished target @{text Quickcheck}
+  not spoiling the regular trusted code generation *}
+
+code_reserved Quickcheck Quickcheck_Generators
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
+
+subsection {* The Random-Predicate Monad *} 
 
 types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
 
@@ -167,24 +182,9 @@
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
   where "map f P = bind P (single o f)"
 
-subsection {* Code setup *}
-
-use "Tools/quickcheck_generators.ML"
-setup {* Quickcheck_Generators.setup *}
-
-code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
-  -- {* With enough criminal energy this can be abused to derive @{prop False};
-  for this reason we use a distinguished target @{text Quickcheck}
-  not spoiling the regular trusted code generation *}
-
-code_reserved Quickcheck Quickcheck_Generators
-
 hide (open) fact empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def
 hide (open) type randompred
 hide (open) const random collapse beyond random_fun_aux random_fun_lift
   empty single bind union if_randompred not_randompred Random map
 
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
-
 end
diff -r 52f30b06938a -r ceeffca32eb0 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Mon Jan 25 19:31:50 2010 +0100
+++ b/src/Tools/Code_Generator.thy	Wed Jan 27 14:02:52 2010 +0100
@@ -29,6 +29,7 @@
   #> Code_Haskell.setup
   #> Code_Scala.setup
   #> Nbe.setup
+  #> Quickcheck.setup
 *}
 
 end