src/HOL/Random_Sequence.thy
 changeset 67091 1393c2340eec parent 60758 d8d85a8172b5
```     1.1 --- a/src/HOL/Random_Sequence.thy	Sun Nov 26 13:19:52 2017 +0100
1.2 +++ b/src/HOL/Random_Sequence.thy	Sun Nov 26 21:08:32 2017 +0100
1.3 @@ -42,7 +42,7 @@
1.4
1.5  definition map :: "('a => 'b) => 'a random_dseq => 'b random_dseq"
1.6  where
1.7 -  "map f P = bind P (single o f)"
1.8 +  "map f P = bind P (single \<circ> f)"
1.9
1.10  fun Random :: "(natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq"
1.11  where
1.12 @@ -82,7 +82,7 @@
1.13
1.14  definition pos_map :: "('a => 'b) => 'a pos_random_dseq => 'b pos_random_dseq"
1.15  where
1.16 -  "pos_map f P = pos_bind P (pos_single o f)"
1.17 +  "pos_map f P = pos_bind P (pos_single \<circ> f)"
1.18
1.19  fun iter :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
1.20    \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
1.21 @@ -132,7 +132,7 @@
1.22
1.23  definition neg_map :: "('a => 'b) => 'a neg_random_dseq => 'b neg_random_dseq"
1.24  where
1.25 -  "neg_map f P = neg_bind P (neg_single o f)"
1.26 +  "neg_map f P = neg_bind P (neg_single \<circ> f)"
1.27
1.28  definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq"
1.29  where
```