changeset 50055 | 94041d602ecb |
parent 42163 | 392fd6c4669c |
--- a/src/HOL/New_Random_Sequence.thy Mon Nov 12 18:42:49 2012 +0100 +++ b/src/HOL/New_Random_Sequence.thy Mon Nov 12 23:24:40 2012 +0100 @@ -2,7 +2,7 @@ (* Author: Lukas Bulwahn, TU Muenchen *) theory New_Random_Sequence -imports Quickcheck New_DSequence +imports Random_Sequence begin type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"