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