Changes

Summary

merged
cleaned proofs

Changeset 71634:03695eeabdde by nipkow: merged
Changeset 71633:07bec530f02e by nipkow: cleaned proofs
The file was modified	`src/HOL/Analysis/Abstract_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Abstract_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Arcwise_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Ball_Volume.thy` (diff)
The file was modified	`src/HOL/Analysis/Bochner_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Borel_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Cartesian_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Change_Of_Vars.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Analysis_Basics.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Cross3.thy` (diff)
The file was modified	`src/HOL/Analysis/Derivative.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Metric_Spaces.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Normed_Spaces.thy` (diff)
The file was modified	`src/HOL/Analysis/Embed_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy` (diff)
The file was modified	`src/HOL/Analysis/Extended_Real_Limits.thy` (diff)
The file was modified	`src/HOL/Analysis/FPS_Convergence.thy` (diff)
The file was modified	`src/HOL/Analysis/Fashoda_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Function_Metric.thy` (diff)
The file was modified	`src/HOL/Analysis/Function_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Further_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Gamma_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Homeomorphism.thy` (diff)
The file was modified	`src/HOL/Analysis/Homotopy.thy` (diff)
The file was modified	`src/HOL/Analysis/Improper_Integral.thy` (diff)
The file was modified	`src/HOL/Analysis/Infinite_Set_Sum.thy` (diff)
The file was modified	`src/HOL/Analysis/Jordan_Curve.thy` (diff)
The file was modified	`src/HOL/Analysis/Lipschitz.thy` (diff)
The file was modified	`src/HOL/Analysis/Measure_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Ordered_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Path_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Analysis/Product_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Regularity.thy` (diff)
The file was modified	`src/HOL/Analysis/Simplex_Content.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Analysis/Summation_Tests.thy` (diff)
The file was modified	`src/HOL/Analysis/Tagged_Division.thy` (diff)
The file was modified	`src/HOL/Analysis/Weierstrass_Theorems.thy` (diff)