Lines Matching refs:SPEC
256 Q.SPEC `(p_space p, events p)`) ALGEBRA_INTER
263 Q.SPEC `(p_space p, events p)`) ALGEBRA_EMPTY
270 Q.SPEC `(p_space p, events p)`) ALGEBRA_SPACE
278 Q.SPEC `(p_space p, events p)`) ALGEBRA_UNION
301 Q.SPEC `(p_space p, events p)`) ALGEBRA_DIFF
309 Q.SPEC `(p_space p, events p)`) ALGEBRA_COMPL
317 Q.SPEC `(p_space p, events p)`) SIGMA_ALGEBRA_COUNTABLE_UNION
613 (prob p s = SIGMA (\x. prob p {x}) s)` (MP_TAC o GSYM o Q.SPEC `p`)
641 >> (MATCH_MP_TAC o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_FINITE_SAME
868 (MP_TAC o Q.SPEC `(\x. PREIMAGE X x INTER p_space p) o f`)
1310 >> (MP_TAC o Q.SPEC `p1` o INST_TYPE [``:'a`` |-> ``:'b``]) PROB_REAL_SUM_IMAGE_SPACE