\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}
\date{}
\maketitle
\noindent
This document is a very compact introduction to structured proofs in
Isar/HOL, an extension of Isabelle/HOL~\cite{LNCS2283}. A detailled
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:
\bibliographystyle{plain}
\bibliography{root}
\end{document}