equal
deleted
inserted
replaced
1 |
1 |
2 (* Author: Lukas Bulwahn, TU Muenchen *) |
2 (* Author: Lukas Bulwahn, TU Muenchen *) |
3 |
3 |
4 theory Random_Sequence |
4 theory Random_Sequence |
5 imports Quickcheck DSequence |
5 imports Quickcheck |
6 begin |
6 begin |
7 |
7 |
8 type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)" |
8 type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)" |
9 |
9 |
10 definition empty :: "'a random_dseq" |
10 definition empty :: "'a random_dseq" |