src/HOL/Random_Sequence.thy
changeset 42163 392fd6c4669c
parent 36176 3fe7e97ccca8
child 50055 94041d602ecb
     1.1 --- a/src/HOL/Random_Sequence.thy	Wed Mar 30 11:32:51 2011 +0200
     1.2 +++ b/src/HOL/Random_Sequence.thy	Wed Mar 30 11:32:52 2011 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  imports Quickcheck DSequence
     1.5  begin
     1.6  
     1.7 -types 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"
     1.8 +type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"
     1.9  
    1.10  definition empty :: "'a random_dseq"
    1.11  where