\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 Structured Proofs in Isar/HOL}
\author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\
 {\small\url{http://www.in.tum.de/~nipkow/}}}
\date{}
\maketitle

\noindent
Isar is an extension of Isabelle with structured proofs in a
stylized language of mathematics. These proofs are readable for both a human
and a machine.

This document is a very compact introduction to structured proofs in
Isar/HOL, an extension of Isabelle/HOL~\cite{LNCS2283}. A detailed
exposition of this material can be found in Markus Wenzel's PhD
thesis~\cite{Wenzel-PhD} and the Isar reference manual~\cite{Isar-Ref-Man}.

\input{Logic.tex}

%\input{Isar.tex}

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

{\small
\paragraph{Acknowledgment}
I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
Stefan Berghofer,
Gerwin Klein, Norbert Schirmer and Markus Wenzel commented on this document.
}

\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{root}
\endgroup

\end{document}
