src/HOL/ex/RPred.thy

 
 definition lift_random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a rpred"
   where "lift_random g = scomp g (Pair o (Predicate.single o fst))"
 
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
-where "map f P = bind P (return o f)"
+  where "map f P = bind P (return o f)"
 
 hide (open) const return bind supp map
   
 end