Changes

Summary

Removal of ugly old proofs
merged
More cosmetic changes
Cosmetic polishing of proofs

Changeset 78477:37abfe400ae6 by paulson _lp15@cam.ac.uk_: Removal of ugly old proofs
The file was modified	`src/HOL/Analysis/Line_Segment.thy` (diff)
Changeset 78476:032a4344903e by paulson: merged
Changeset 78475:a5f6d2fc1b1f by paulson _lp15@cam.ac.uk_: More cosmetic changes
The file was modified	`src/HOL/Analysis/Bochner_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Brouwer_Fixpoint.thy` (diff)
The file was modified	`src/HOL/Analysis/Change_Of_Vars.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex.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/Elementary_Topology.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/Smooth_Paths.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Conformal_Mappings.thy` (diff)
Changeset 78474:cc1058b83124 by paulson _lp15@cam.ac.uk_: Cosmetic polishing of proofs
The file was modified	`src/HOL/Analysis/Homotopy.thy` (diff)
The file was modified	`src/HOL/Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Analysis/Tagged_Division.thy` (diff)