src/HOL/Quickcheck.thy
changeset 45178 fe9993491317
parent 45159 3f1d1ce024cb
child 45718 8979b2463fc8
equal deleted inserted replaced
45177:189c81779a68 45178:fe9993491317
   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 *}
       
   153 
       
   154 subsection {* The Random-Predicate Monad *} 
   147 subsection {* The Random-Predicate Monad *} 
   155 
   148 
   156 fun iter' ::
   149 fun iter' ::
   157   "'a itself => code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred"
   150   "'a itself => code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred"
   158 where
   151 where