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