src/HOL/ex/CodeRandom.thy
changeset 21876 96a601bc59d8
parent 21545 54cc492d80a9
child 21912 ff45788e7bf9
equal deleted inserted replaced
21875:5df10a17644e 21876:96a601bc59d8
   187   (SML "case _ (Random.seed ()) of (x, '_) => x")
   187   (SML "case _ (Random.seed ()) of (x, '_) => x")
   188 
   188 
   189 code_gen select select_weight
   189 code_gen select select_weight
   190   (SML #)
   190   (SML #)
   191 
   191 
   192 code_gen (SML -)
       
   193 
       
   194 end
   192 end