src/HOL/Quickcheck.thy
changeset 45159 3f1d1ce024cb
parent 44845 5e51075cbd97
child 45178 fe9993491317
equal deleted inserted replaced
45157:efc2e2d80218 45159:3f1d1ce024cb
   142 code_reserved Quickcheck Random_Generators
   142 code_reserved Quickcheck Random_Generators
   143 
   143 
   144 no_notation fcomp (infixl "\<circ>>" 60)
   144 no_notation fcomp (infixl "\<circ>>" 60)
   145 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   145 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   146 
   146 
       
   147 subsection {* Tester SML-inductive based on the SML code generator *}
       
   148 
       
   149 setup {*
       
   150   Context.theory_map (Quickcheck.add_tester ("SML_inductive",
       
   151     (Inductive_Codegen.active, Quickcheck_Common.generator_test_goal_terms Inductive_Codegen.test_term)));
       
   152 *}
   147 
   153 
   148 subsection {* The Random-Predicate Monad *} 
   154 subsection {* The Random-Predicate Monad *} 
   149 
   155 
   150 fun iter' ::
   156 fun iter' ::
   151   "'a itself => code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred"
   157   "'a itself => code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred"