| changeset 36649 | bfd8c550faa6 |
| parent 35704 | 5007843dae33 |
| child 37032 | 58a0757031dd |
--- a/src/HOL/Probability/Caratheodory.thy Tue May 04 18:05:22 2010 +0200 +++ b/src/HOL/Probability/Caratheodory.thy Tue May 04 18:19:24 2010 +0200 @@ -1,7 +1,7 @@ header {*Caratheodory Extension Theorem*} theory Caratheodory - imports Sigma_Algebra SupInf SeriesPlus + imports Sigma_Algebra SeriesPlus begin text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}