\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}

%for best-style documents ...
\urlstyle{rm}
%\isabellestyle{it}

\newtheorem{Exercise}{Exercise}[section]
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}

\begin{document}

\title{A Compact Overview of Isabelle/HOL}
\author{Tobias Nipkow}
\date{}
\maketitle

\noindent
This document is a very compact introduction to the proof assistant
Isabelle/HOL and is based directly on the published tutorial~\cite{LNCS2283}
where full explanations and a wealth of additional material can be found.

While reading this document it is recommended to single-step through the
corresponding theories using Isabelle/HOL to follow the proofs.

\section{Functional Programming/Modelling}

\subsection{An Introductory Theory}
\input{FP0.tex}

\subsection{More Constructs}
\input{FP1.tex}

\input{RECDEF.tex}

\input{Rules.tex}

\input{Sets.tex}

\input{Ind.tex}

%\input{Isar.tex}

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


\bibliographystyle{plain}
\bibliography{root}

\end{document}
