src/HOL/Quickcheck.thy
changeset 44845 5e51075cbd97
parent 42175 32c3bb5e1b1a
child 45159 3f1d1ce024cb
equal deleted inserted replaced
44844:f74a4175a3a8 44845:5e51075cbd97
   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