equal
deleted
inserted
replaced
181 |
181 |
182 definition union :: "'a randompred \<Rightarrow> 'a randompred \<Rightarrow> 'a randompred" |
182 definition union :: "'a randompred \<Rightarrow> 'a randompred \<Rightarrow> 'a randompred" |
183 where |
183 where |
184 "union R1 R2 = (\<lambda>s. let |
184 "union R1 R2 = (\<lambda>s. let |
185 (P1, s') = R1 s; (P2, s'') = R2 s' |
185 (P1, s') = R1 s; (P2, s'') = R2 s' |
186 in (semilattice_sup_class.sup P1 P2, s''))" |
186 in (sup_class.sup P1 P2, s''))" |
187 |
187 |
188 definition if_randompred :: "bool \<Rightarrow> unit randompred" |
188 definition if_randompred :: "bool \<Rightarrow> unit randompred" |
189 where |
189 where |
190 "if_randompred b = (if b then single () else empty)" |
190 "if_randompred b = (if b then single () else empty)" |
191 |
191 |