equal
deleted
inserted
replaced
1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 section \<open>A HOL random engine\<close> |
3 section \<open>A HOL random engine\<close> |
4 |
4 |
5 theory Random |
5 theory Random |
6 imports List Groups_List |
6 imports List Groups_List Code_Numeral |
7 begin |
7 begin |
8 |
8 |
9 subsection \<open>Auxiliary functions\<close> |
9 subsection \<open>Auxiliary functions\<close> |
10 |
10 |
11 fun log :: "natural \<Rightarrow> natural \<Rightarrow> natural" where |
11 fun log :: "natural \<Rightarrow> natural \<Rightarrow> natural" where |