Session Hybrid_Systems_VCs

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