| changeset 57242 | 25aff3b8d550 |
| parent 57225 | ff69e42ccf92 |
| child 58101 | e7ebe5554281 |
| 57241:7fca4159117f | 57242:25aff3b8d550 |
|---|---|
2 (* Author: Florian Haftmann, TU Muenchen *) |
2 (* Author: Florian Haftmann, TU Muenchen *) |
3 |
3 |
4 header {* A HOL random engine *} |
4 header {* A HOL random engine *} |
5 |
5 |
6 theory Random |
6 theory Random |
7 imports Code_Numeral List |
7 imports List |
8 begin |
8 begin |
9 |
9 |
10 notation fcomp (infixl "\<circ>>" 60) |
10 notation fcomp (infixl "\<circ>>" 60) |
11 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
11 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
12 |
12 |