Session Hybrid_Systems_VCs
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
HS_Preliminaries
HS_ODEs
HS_VC_Spartan
HS_VC_Examples
Order_Lattice_Props.Sup_Lattice
Order_Lattice_Props.Order_Duality
Order_Lattice_Props.Order_Lattice_Props
Transformer_Semantics.Powerset_Monad
Order_Lattice_Props.Galois_Connections
Order_Lattice_Props.Fixpoint_Fusion
Order_Lattice_Props.Closure_Operators
Kleene_Algebra.Signatures
Kleene_Algebra.Dioid
Quantales.Quantales
Kleene_Algebra.Conway
Kleene_Algebra.Kleene_Algebra
Quantales.Quantale_Star
Transformer_Semantics.Isotone_Transformers
Transformer_Semantics.Sup_Inf_Preserving_Transformers
Transformer_Semantics.Kleisli_Transformers
Transformer_Semantics.Kleisli_Quantaloid
HS_VC_PT
HS_VC_PT_Examples
KAD.Domain_Semiring
KAD.Antidomain_Semiring
KAD.Range_Semiring
KAD.Modal_Kleene_Algebra
HS_VC_MKA
HS_VC_KA_rel
HS_VC_MKA_rel
HS_VC_MKA_Examples_rel
Transformer_Semantics.Kleisli_Quantale
HS_VC_KA_ndfun
HS_VC_MKA_ndfun
HS_VC_MKA_Examples_ndfun
KAT_and_DRA.Test_Dioid
KAT_and_DRA.Conway_Tests
KAT_and_DRA.KAT
Kleene_Algebra.PHL_KA
KAT_and_DRA.PHL_KAT
HS_VC_KAT
HS_VC_KAT_rel
HOL-Eisbach.Eisbach
File ‹parse_tools.ML›
File ‹method_closure.ML›
File ‹eisbach_rule_insts.ML›
File ‹match_method.ML›
HS_VC_KAT_Examples_rel
HS_VC_KAT_ndfun
HS_VC_KAT_Examples_ndfun