src/HOL/Analysis/Measure_Space.thy
changeset 69517 dc20f278e8f3
parent 69313 b021008c5397
child 69541 d466e0a639e4
equal deleted inserted replaced
69516:09bb8f470959 69517:dc20f278e8f3
     2     Author:     Lawrence C Paulson
     2     Author:     Lawrence C Paulson
     3     Author:     Johannes Hölzl, TU München
     3     Author:     Johannes Hölzl, TU München
     4     Author:     Armin Heller, TU München
     4     Author:     Armin Heller, TU München
     5 *)
     5 *)
     6 
     6 
     7 section \<open>Measure spaces and their properties\<close>
     7 section \<open>Measure Spaces\<close>
     8 
     8 
     9 theory Measure_Space
     9 theory Measure_Space
    10 imports
    10 imports
    11   Measurable "HOL-Library.Extended_Nonnegative_Real"
    11   Measurable "HOL-Library.Extended_Nonnegative_Real"
    12 begin
    12 begin