Changes

Summary

merged
new material about topology, etc.; also fixes for yesterday's

Changeset 69923:cd8b6f32ed79 by paulson: merged
Changeset 69922:4a9167f377b0 by paulson _lp15@cam.ac.uk_: new material about topology, etc.; also fixes for yesterday's
The file was added	`src/HOL/Analysis/Product_Topology.thy`
The file was modified	`src/HOL/Analysis/Abstract_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Abstract_Topology_2.thy` (diff)
The file was modified	`src/HOL/Analysis/Analysis.thy` (diff)
The file was modified	`src/HOL/Analysis/Arcwise_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Brouwer_Fixpoint.thy` (diff)
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Change_Of_Vars.thy` (diff)
The file was modified	`src/HOL/Analysis/Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Continuous_Extension.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex_Euclidean_Space.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/Equivalence_Lebesgue_Henstock_Integration.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/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/Jordan_Curve.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Analysis/Riemann_Mapping.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Vitali_Covering_Theorem.thy` (diff)
The file was modified	`src/HOL/Product_Type.thy` (diff)