equal
deleted
inserted
replaced
260 |
260 |
261 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)" |
261 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)" |
262 where "map f P = bind P (single o f)" |
262 where "map f P = bind P (single o f)" |
263 |
263 |
264 hide_fact |
264 hide_fact |
265 random_bool_def random_bool_def_raw |
265 random_bool_def |
266 random_itself_def random_itself_def_raw |
266 random_itself_def |
267 random_char_def random_char_def_raw |
267 random_char_def |
268 random_literal_def random_literal_def_raw |
268 random_literal_def |
269 random_nat_def random_nat_def_raw |
269 random_nat_def |
270 random_int_def random_int_def_raw |
270 random_int_def |
271 random_fun_lift_def random_fun_lift_def_raw |
271 random_fun_lift_def |
272 random_fun_def random_fun_def_raw |
272 random_fun_def |
273 collapse_def collapse_def_raw |
273 collapse_def |
274 beyond_def beyond_def_raw beyond_zero |
274 beyond_def |
|
275 beyond_zero |
275 random_aux_rec |
276 random_aux_rec |
276 |
277 |
277 hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift |
278 hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift |
278 |
279 |
279 hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def |
280 hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def |