Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. New material (and some tidying) purely in the Analysis directory
  2. Merge
  3. Some fixes related to compactE_image
  4. Merge
  5. Further new material. The simprule status of some exp and ln identities was reverted.
Changeset 65587:16a8991ab398 by paulson _lp15@cam.ac.uk_:
New material (and some tidying) purely in the Analysis directory
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.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/Equivalence_Lebesgue_Henstock_Integration.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/Topology_Euclidean_Space.thy (diff)
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)