\chapter{Preface}

This document contains the automatically generated listings of the
Isabelle sources for the theories defining and analysing Jinja (a
Java-like programming language), the Jinja Virtual Machine, and the
compiler. To shorten the document, all proofs have been hidden.  For a
detailed exposition of these theories see the paper by Klein and
Nipkow~\cite{KleinN04,KleinN-Toplas}.


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
