Changes

Summary

new lemma
dedicated append function for string literals
generalized
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements

Changeset 67730:f91c437f6f68 by haftmann: new lemma
The file was modified	`src/HOL/Library/More_List.thy` (diff)
The file was modified	`src/HOL/String.thy` (diff)
Changeset 67729:5152afa6258f by haftmann: dedicated append function for string literals
The file was modified	`src/HOL/String.thy` (diff)
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 added	`src/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)