equal
deleted
inserted
replaced
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 |