changeset 74101 | d804e93ae9ff |
parent 72581 | de581f98a3a1 |
child 80175 | 200107cdd3ac |
--- a/src/HOL/Random.thy Sun Aug 01 23:18:13 2021 +0200 +++ b/src/HOL/Random.thy Mon Aug 02 10:01:06 2021 +0000 @@ -3,7 +3,7 @@ section \<open>A HOL random engine\<close> theory Random -imports List Groups_List +imports List Groups_List Code_Numeral begin subsection \<open>Auxiliary functions\<close>