| changeset 59361 | fd5da2434be4 |
| parent 59353 | f0707dc3d9aa |
| child 60172 | 423273355b55 |
--- a/src/HOL/Probability/Measurable.thy Wed Jan 14 17:04:19 2015 +0100 +++ b/src/HOL/Probability/Measurable.thy Thu Jan 15 15:04:51 2015 +0100 @@ -97,6 +97,7 @@ declare measurable_cong_sets[measurable_cong] declare sets_restrict_space_cong[measurable_cong] +declare sets_restrict_UNIV[measurable_cong] lemma predE[measurable (raw)]: "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"