Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
make random engine persistent using code_reflect
authorhaftmann
Thu, 29 Apr 2010 15:22:16 +0200
changeset 36538 4fe16d49283b
parent 36537 b0186c66f324
child 36539 2b9d4d3f09c3
make random engine persistent using code_reflect
src/HOL/Random.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Random.thy	Thu Apr 29 15:00:43 2010 +0200
+++ b/src/HOL/Random.thy	Thu Apr 29 15:22:16 2010 +0200
@@ -138,10 +138,15 @@
 
 subsection {* @{text ML} interface *}
 
+code_reflect Random_Engine
+  functions range select select_weight
+
 ML {*
 structure Random_Engine =
 struct
 
+open Random_Engine;
+
 type seed = int * int;
 
 local
isabelle