src/HOL/Random.thy
changeset 42163 392fd6c4669c
parent 39302 d7728f65b353
child 44921 58eef4843641
     1.1 --- a/src/HOL/Random.thy	Wed Mar 30 11:32:51 2011 +0200
     1.2 +++ b/src/HOL/Random.thy	Wed Mar 30 11:32:52 2011 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  
     1.5  subsection {* Random seeds *}
     1.6  
     1.7 -types seed = "code_numeral \<times> code_numeral"
     1.8 +type_synonym seed = "code_numeral \<times> code_numeral"
     1.9  
    1.10  primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
    1.11    "next (v, w) = (let