Changes

Summary

some new material, also recasting some theorems using “obtains”
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion

Changeset 65037:2cf841ff23be by paulson _lp15@cam.ac.uk_: some new material, also recasting some theorems using “obtains”
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Further_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Uniform_Limit.thy` (diff)
Changeset 65036:ab7e11730ad8 by paulson _lp15@cam.ac.uk_: Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
The file was modified	`src/HOL/Analysis/Bounded_Continuous_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Conformal_Mappings.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Function_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Uniform_Limit.thy` (diff)
The file was modified	`src/HOL/Limits.thy` (diff)
The file was modified	`src/HOL/Real_Vector_Spaces.thy` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)