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