| changeset 63464 | 9d4dbb7a548a |
| parent 63329 | 6b26c378ab35 |
| child 63970 | 3b6a3632e754 |
--- a/src/HOL/Probability/Distribution_Functions.thy Tue Jul 12 16:04:19 2016 +0200 +++ b/src/HOL/Probability/Distribution_Functions.thy Tue Jul 12 19:12:17 2016 +0200 @@ -17,7 +17,7 @@ should be somewhere else. *) theory Distribution_Functions - imports Probability_Measure "~~/src/HOL/Library/ContNotDenum" + imports Probability_Measure "~~/src/HOL/Library/Continuum_Not_Denumerable" begin lemma UN_Ioc_eq_UNIV: "(\<Union>n. { -real n <.. real n}) = UNIV"