1.1 --- a/src/HOL/ex/RPred.thy	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/ex/RPred.thy	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -14,13 +14,15 @@
     1.4  definition return :: "'a => 'a rpred"
     1.5    where "return x = Pair (Predicate.single x)"
     1.6  
     1.7 -definition bind :: "'a rpred \<Rightarrow> ('a \<Rightarrow> 'b rpred) \<Rightarrow> 'b rpred" (infixl "\<guillemotright>=" 60)
     1.8 +definition bind :: "'a rpred \<Rightarrow> ('a \<Rightarrow> 'b rpred) \<Rightarrow> 'b rpred"
     1.9 +(* (infixl "\<guillemotright>=" 60) *)
    1.10    where "bind RP f =
    1.11    (\<lambda>s. let (P, s') = RP s;
    1.12          (s1, s2) = Random.split_seed s'
    1.13      in (Predicate.bind P (%a. fst (f a s1)), s2))"
    1.14  
    1.15 -definition supp :: "'a rpred \<Rightarrow> 'a rpred \<Rightarrow> 'a rpred" (infixl "\<squnion>" 80)
    1.16 +definition supp :: "'a rpred \<Rightarrow> 'a rpred \<Rightarrow> 'a rpred"
    1.17 +(* (infixl "\<squnion>" 80) *)
    1.18  where
    1.19    "supp RP1 RP2 = (\<lambda>s. let (P1, s') = RP1 s; (P2, s'') = RP2 s'
    1.20    in (upper_semilattice_class.sup P1 P2, s''))"
    1.21 @@ -43,6 +45,8 @@
    1.22    where "lift_random g = scomp g (Pair o (Predicate.single o fst))"
    1.23  
    1.24  definition map_rpred :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
    1.25 -where "map_rpred f P = P \<guillemotright>= (return o f)"
    1.26 +where "map_rpred f P = bind P (return o f)"
    1.27 +
    1.28 +hide (open) const return bind supp 
    1.29    
    1.30  end
    1.31 \ No newline at end of file