make random engine persistent using code_reflect
authorhaftmann
Thu Apr 29 15:22:16 2010 +0200 (2010-04-29)
changeset 365384fe16d49283b
parent 36537 b0186c66f324
child 36539 2b9d4d3f09c3
make random engine persistent using code_reflect
src/HOL/Random.thy
     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