Changes

Summary

move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel

Changeset 63886:685fb01256af by hoelzl: move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
The file was added	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy`
The file was modified	`src/HOL/Analysis/Bochner_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Cartesian_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Analysis_Basics.thy` (diff)
The file was modified	`src/HOL/Analysis/Derivative.thy` (diff)
The file was modified	`src/HOL/Analysis/Embed_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Interval_Integral.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Linear_Algebra.thy` (diff)
The file was modified	`src/HOL/Analysis/Ordered_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Set_Integral.thy` (diff)
The file was modified	`src/HOL/Library/Inner_Product.thy` (diff)
The file was modified	`src/HOL/Probability/Characteristic_Functions.thy` (diff)
The file was modified	`src/HOL/Probability/Distributions.thy` (diff)
The file was modified	`src/HOL/Probability/Giry_Monad.thy` (diff)
The file was modified	`src/HOL/Probability/Information.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/Probability_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/SPMF.thy` (diff)
The file was modified	`src/HOL/Probability/Sinc_Integral.thy` (diff)