Session Ordinary_Differential_Equations

Theories

• HOL-Library.Lattice_Algebras
• HOL-Library.Interval
• HOL-Library.Log_Nat
• HOL-Library.Float
• HOL-Library.Interval_Float
• HOL-Decision_Procs.Dense_Linear_Order
  • File ‹langford_data.ML›
  • File ‹ferrante_rackoff_data.ML›
  • File ‹langford.ML›
  • File ‹ferrante_rackoff.ML›
• HOL-Decision_Procs.Approximation_Bounds
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Int
• HOL-Library.Code_Target_Bit_Shifts
• HOL-Library.Code_Target_Numeral
• HOL-Library.Code_Target_Numeral_Float
• HOL-Decision_Procs.Approximation
  • File ‹approximation.ML›
  • File ‹approximation_generator.ML›
• List-Index.List_Index
• Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
• HOL-Library.Code_Cardinality
• Affine_Arithmetic.Executable_Euclidean_Space
• ODE_Auxiliarities
• MVT_Ex
• Vector_Derivative_On
• Interval_Integral_HK
• Gronwall
• Initial_Value_Problem
• Picard_Lindeloef_Qualitative
• HOL-Library.Diagonal_Subsequence
• Bounded_Linear_Operator
• Multivariate_Taylor
• Flow
• Upper_Lower_Solution
• Poincare_Map
• Reachability_Analysis
• Flow_Congs
• Triangle.Angles
• Triangle.Triangle
• Cones
• Linear_ODE
• ODE_Analysis