src/HOL/Random_Sequence.thy
changeset 50055 94041d602ecb
parent 42163 392fd6c4669c
child 51126 df86080de4cb
     1.1 --- a/src/HOL/Random_Sequence.thy	Mon Nov 12 18:42:49 2012 +0100
     1.2 +++ b/src/HOL/Random_Sequence.thy	Mon Nov 12 23:24:40 2012 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4  (* Author: Lukas Bulwahn, TU Muenchen *)
     1.5  
     1.6  theory Random_Sequence
     1.7 -imports Quickcheck DSequence
     1.8 +imports Quickcheck
     1.9  begin
    1.10  
    1.11  type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"