Lines Matching defs:HOL
4 This document describes a link between Isabelle/HOL and the \SPARK{}/Ada tool
8 can be found in the directory \texttt{HOL/SPARK/Examples} in the Isabelle
13 we give an introduction to \SPARK{} and the HOL-\SPARK{} link. The verification
17 describes the commands provided by the HOL-\SPARK{} link, as well as the encoding
18 of \SPARK{} types in HOL.
64 \section{HOL-\SPARK{}}
66 The HOL-\SPARK{} verification environment, which is built on top of Isabelle's object
67 logic HOL, is intended as an alternative
69 HOL-\SPARK{} allows Isabelle to directly parse files generated
92 \node[rbox] (isa) at (5,-10) {HOL-\SPARK{}};
120 Figure \ref{fig:spark-toolchain} shows the integration of HOL-\SPARK{} into the
121 tool chain for the verification of \SPARK{} programs. HOL-\SPARK{} processes declarations