Lines Matching defs:SPACE
221 val SPACE = store_thm
222 ("SPACE",
818 >> REWRITE_TAC [measurable_sets_def, m_space_def, SPACE]
1389 >> RW_TAC std_ss [SPACE]);
1498 >> CONJ_TAC >- RW_TAC std_ss [measurable_sets_def, subsets_def, space_def, m_space_def, SPACE]
1504 >> REWRITE_TAC [measurable_sets_def, measure_def, space_def, m_space_def, subsets_def, SPACE]
2255 PROVE_TAC [SPACE_SIGMA, SPACE]);
2463 >- RW_TAC std_ss [SPACE]
2567 RW_TAC std_ss [IN_MEASURABLE, I_THM, PREIMAGE_I, IN_FUNSET, GSPEC_ID, SPACE, SUBSET_REFL]
2681 measure_def, measurable_sets_def, m_space_def, SPACE]
2832 IN_FUNSET, IN_UNIV, measure_space_def, m_space_def, SPACE]
2858 measure_def, SIGMA_ALGEBRA_ALGEBRA, SPACE])
4052 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, space_def, subsets_def, SPACE])