  We present a semantic framework for the deductive verification of hybrid
systems with Isabelle/HOL. It supports reasoning about the temporal evolutions
of hybrid programs in the style of differential dynamic logic modelled by flows
or invariant sets for vector fields. We introduce the semantic foundations of
this framework and summarise their Isabelle formalisation as well as the
resulting verification components. A series of simple examples shows our
approach at work.
