Changes

Summary

Probability: move emeasure and nn_integral from ereal to ennreal

Changeset 62975:1d066f6ab25d by hoelzl: Probability: move emeasure and nn_integral from ereal to ennreal
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Real.thy` (diff)
The file was modified	`src/HOL/Library/Liminf_Limsup.thy` (diff)
The file was modified	`src/HOL/Probability/Binary_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Bochner_Integration.thy` (diff)
The file was modified	`src/HOL/Probability/Borel_Space.thy` (diff)
The file was modified	`src/HOL/Probability/Caratheodory.thy` (diff)
The file was modified	`src/HOL/Probability/Complete_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Convolution.thy` (diff)
The file was modified	`src/HOL/Probability/Distribution_Functions.thy` (diff)
The file was modified	`src/HOL/Probability/Distributions.thy` (diff)
The file was modified	`src/HOL/Probability/Embed_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Giry_Monad.thy` (diff)
The file was modified	`src/HOL/Probability/Independent_Family.thy` (diff)
The file was modified	`src/HOL/Probability/Infinite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Information.thy` (diff)
The file was modified	`src/HOL/Probability/Lebesgue_Integral_Substitution.thy` (diff)
The file was modified	`src/HOL/Probability/Lebesgue_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Levy.thy` (diff)
The file was modified	`src/HOL/Probability/Measurable.thy` (diff)
The file was modified	`src/HOL/Probability/Measure_Space.thy` (diff)
The file was modified	`src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Projective_Family.thy` (diff)
The file was modified	`src/HOL/Probability/Projective_Limit.thy` (diff)
The file was modified	`src/HOL/Probability/Radon_Nikodym.thy` (diff)
The file was modified	`src/HOL/Probability/Regularity.thy` (diff)
The file was modified	`src/HOL/Probability/Sigma_Algebra.thy` (diff)
The file was modified	`src/HOL/Probability/Sinc_Integral.thy` (diff)
The file was modified	`src/HOL/Probability/Weak_Convergence.thy` (diff)