src/HOL/Random.thy
changeset 36538 4fe16d49283b
parent 36176 3fe7e97ccca8
child 37751 89e16802b6cc
     1.1 --- a/src/HOL/Random.thy	Thu Apr 29 15:00:43 2010 +0200
     1.2 +++ b/src/HOL/Random.thy	Thu Apr 29 15:22:16 2010 +0200
     1.3 @@ -138,10 +138,15 @@
     1.4  
     1.5  subsection {* @{text ML} interface *}
     1.6  
     1.7 +code_reflect Random_Engine
     1.8 +  functions range select select_weight
     1.9 +
    1.10  ML {*
    1.11  structure Random_Engine =
    1.12  struct
    1.13  
    1.14 +open Random_Engine;
    1.15 +
    1.16  type seed = int * int;
    1.17  
    1.18  local