| changeset 24994 | c385c4eabb3b |
| parent 24630 | 351a308ab58d |
| child 26038 | 55a02586776d |
| 24993:92dfacb32053 | 24994:c385c4eabb3b |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* A simple random engine *} |
5 header {* A simple random engine *} |
6 |
6 |
7 theory Random |
7 theory Random |
8 imports State_Monad Pretty_Int |
8 imports State_Monad Code_Integer |
9 begin |
9 begin |
10 |
10 |
11 fun |
11 fun |
12 pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a" |
12 pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a" |
13 where |
13 where |