src/HOL/New_Random_Sequence.thy
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"