Session Matrices_for_ODEs
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Log_Nat
HOL-Library.Lattice_Algebras
HOL-Library.Float
List-Index.List_Index
Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
HOL-Library.Code_Cardinality
Affine_Arithmetic.Executable_Euclidean_Space
Ordinary_Differential_Equations.ODE_Auxiliarities
Ordinary_Differential_Equations.Vector_Derivative_On
Ordinary_Differential_Equations.Interval_Integral_HK
Ordinary_Differential_Equations.Gronwall
Ordinary_Differential_Equations.Initial_Value_Problem
Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
Hybrid_Systems_VCs.HS_Preliminaries
MTX_Preliminaries
MTX_Norms
SQ_MTX
Hybrid_Systems_VCs.HS_ODEs
MTX_Flows
Hybrid_Systems_VCs.HS_VC_Spartan
MTX_Examples