Changes

Summary

merged
Probability builds with new definitions
Analysis builds using set_borel_measurable_def, etc.
merged
replacement of set integral abbreviations by actual definitions!
added lemma

Changeset 67978:06bce659d41b by paulson: merged
Changeset 67977:557ea2740125 by paulson _lp15@cam.ac.uk_: Probability builds with new definitions
The file was modified	`src/HOL/Analysis/Set_Integral.thy` (diff)
The file was modified	`src/HOL/Probability/Characteristic_Functions.thy` (diff)
The file was modified	`src/HOL/Probability/Conditional_Expectation.thy` (diff)
The file was modified	`src/HOL/Probability/Distributions.thy` (diff)
The file was modified	`src/HOL/Probability/Levy.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Probability/Sinc_Integral.thy` (diff)
Changeset 67976:75b94eb58c3d by paulson _lp15@cam.ac.uk_: Analysis builds using set_borel_measurable_def, etc.
The file was modified	`src/HOL/Analysis/Ball_Volume.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Gamma_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Integral_Substitution.thy` (diff)
Changeset 67975:27c8692825f6 by paulson: merged
Changeset 67974:3f352a91b45a by paulson _lp15@cam.ac.uk_: replacement of set integral abbreviations by actual definitions!
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Infinite_Set_Sum.thy` (diff)
The file was modified	`src/HOL/Analysis/Interval_Integral.thy` (diff)
The file was modified	`src/HOL/Analysis/Set_Integral.thy` (diff)
Changeset 67973:9ecc78bcf1ef by nipkow: added lemma
The file was modified	`src/HOL/List.thy` (diff)