Changes

Summary

Merge
Some fixes related to compactE_image
Merge
Further new material. The simprule status of some exp and ln identities was reverted.

Changeset 65586:91e451bc0f1f by paulson _lp15@cam.ac.uk_: Merge
Changeset 65585:a043de9ad41e by paulson _lp15@cam.ac.uk_: Some fixes related to compactE_image
The file was modified	`src/HOL/Analysis/Brouwer_Fixpoint.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Weierstrass_Theorems.thy` (diff)
Changeset 65584:1d9a96750a40 by paulson _lp15@cam.ac.uk_: Merge
Changeset 65583:8d53b3bebab4 by paulson _lp15@cam.ac.uk_: Further new material. The simprule status of some exp and ln identities was reverted.
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/Generalised_Binomial_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Weierstrass_Theorems.thy` (diff)
The file was modified	`src/HOL/Complex.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Primes.thy` (diff)
The file was modified	`src/HOL/Library/Float.thy` (diff)
The file was modified	`src/HOL/Matrix_LP/ComputeFloat.thy` (diff)
The file was modified	`src/HOL/Nat.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)