Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. generalized
  2. moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
Changeset 67728:d97a28a006f9 by immler:
generalized
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
Changeset 67727:ce3e87a51488 by immler:
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
The file was addedsrc/HOL/Analysis/Lipschitz.thy
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Lattices.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)