Changes

Summary

merged
A subtle fix involving the "measurable" attribute
merged
Numerous minor tweaks and simplifications
substantial tidy-up, shortening many proofs
add Go component

Changeset 78520:3a4ff63a2537 by paulson: merged
Changeset 78519:f675e2a31682 by paulson _lp15@cam.ac.uk_: A subtle fix involving the "measurable" attribute
The file was modified	`src/HOL/Analysis/Borel_Space.thy` (diff)
Changeset 78518:9c547cdf8379 by paulson: merged
Changeset 78517:28c1f4f5335f by paulson _lp15@cam.ac.uk_: Numerous minor tweaks and simplifications
The file was modified	`src/HOL/Analysis/Abstract_Topological_Spaces.thy` (diff)
The file was modified	`src/HOL/Analysis/Path_Connected.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Complex_Singularities.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Conformal_Mappings.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Contour_Integration.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Laurent_Convergence.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Residue_Theorem.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Riemann_Mapping.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/SPMF.thy` (diff)
Changeset 78516:56a408fa2440 by paulson _lp15@cam.ac.uk_: substantial tidy-up, shortening many proofs
The file was modified	`src/HOL/Analysis/Affine.thy` (diff)
The file was modified	`src/HOL/Analysis/Borel_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Analysis_Basics.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Further_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Homotopy.thy` (diff)
The file was modified	`src/HOL/Probability/Infinite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)
Changeset 78515:c9fb5e7975c5 by Lars Hupel _lars@hupel.info_: add Go component
The file was modified	`Admin/components/components.sha1` (diff)