Changes

Summary

merged
moved auxiliary lemmas

Changeset 8920:d961a099a3fa by immler: merged
Changeset 8919:c96d35967a9b by immler: moved auxiliary lemmas
The file was added	`thys/Ordinary_Differential_Equations/Library/Gronwall.thy`
The file was added	`thys/Ordinary_Differential_Equations/Library/Interval_Integral_HK.thy`
The file was added	`thys/Ordinary_Differential_Equations/Library/Vector_Derivative_On.thy`
The file was modified	`thys/Affine_Arithmetic/Affine_Arithmetic_Auxiliarities.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Floatarith_Expression.thy` (diff)
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/Green/Paths.thy` (diff)
The file was modified	`thys/Gromov_Hyperbolicity/Isometries.thy` (diff)
The file was modified	`thys/List-Infinite/CommonSet/SetInterval2.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Cones.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/IVP/Poincare_Map.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Reachability_Analysis.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Upper_Lower_Solution.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Library/Multivariate_Taylor.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy` (diff)