\documentclass[envcountsame]{llncs}
%\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}
%for best-style documents ...
\urlstyle{rm}
%\isabellestyle{it}
\begin{document}
\title{A Compact Introduction to Structured Proofs in Isar/HOL}
\author{Tobias Nipkow}
\institute{Institut f{\"u}r Informatik, TU M{\"u}nchen\\
{\small\url{http://www.in.tum.de/~nipkow/}}}
\date{}
\maketitle
\begin{abstract}
Isar is an extension of the theorem prover Isabelle with a language
for writing human-readable structured proofs. This paper is an
introduction to the basic constructs of this language. It is aimed
at potential users of Isar but also discusses the design rationals
behind the language and its constructs.
\end{abstract}
\input{intro.tex}
\input{Logic.tex}
\input{Induction.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,
Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer and
Markus Wenzel commented on and improved this document.
}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{root}
\endgroup
\end{document}