src/HOL/Analysis/Caratheodory.thy
changeset 69517 dc20f278e8f3
parent 69325 4b6ddc5989fc
child 69546 27dae626822b
equal deleted inserted replaced
69516:09bb8f470959 69517:dc20f278e8f3
     4 *)
     4 *)
     5 
     5 
     6 section%important \<open>Caratheodory Extension Theorem\<close>
     6 section%important \<open>Caratheodory Extension Theorem\<close>
     7 
     7 
     8 theory Caratheodory
     8 theory Caratheodory
     9   imports Measure_Space
     9 imports Measure_Space
    10 begin
    10 begin
    11 
    11 
    12 text \<open>
    12 text \<open>
    13   Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
    13   Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
    14 \<close>
    14 \<close>