Changes

Summary

more readable proof
removed workaround for code-generation problem, by using Florian's fix in 3817a93a3e5e
merged
moved Lipschitz continuity and Gromov_Hyperbolicity/Library_Complements

Changeset 8946:c0ea770b5d21 by nipkow: more readable proof
The file was modified	`thys/Amortized_Complexity/Pairing_Heap_Tree_Analysis.thy` (diff)
Changeset 8945:73cccdabdfa4 by rene thiemann _rene.thiemann@uibk.ac.at_: removed workaround for code-generation problem, by using Florian's fix in 3817a93a3e5e
The file was modified	`thys/LLL_Factorization/Factorization_Algorithm_16_22.thy` (diff)
Changeset 8944:976ddee7d70f by immler: merged
Changeset 8943:f8e95f71de99 by immler: moved Lipschitz continuity and Gromov_Hyperbolicity/Library_Complements
The file was modified	`thys/Differential_Dynamic_Logic/Differential_Axioms.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Lib.thy` (diff)
The file was modified	`thys/Gromov_Hyperbolicity/Eexp_Eln.thy` (diff)
The file was modified	`thys/Gromov_Hyperbolicity/Gromov_Boundary.thy` (diff)
The file was modified	`thys/Gromov_Hyperbolicity/Gromov_Hyperbolicity.thy` (diff)
The file was modified	`thys/Gromov_Hyperbolicity/Isometries.thy` (diff)
The file was modified	`thys/Gromov_Hyperbolicity/Library_Complements.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Flow.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Library/Vector_Derivative_On.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/One_Step_Method.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy` (diff)