\documentclass[envcountsame]{llncs}
%\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}
%for best-style documents ...
\urlstyle{rm}
%\isabellestyle{it}
\newcommand{\tweakskip}{\vspace{-\medskipamount}}
\newcommand{\Tweakskip}{\tweakskip\tweakskip}
\pagestyle{plain}
\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}
\Tweakskip\Tweakskip
\input{Induction.tex}
\Tweakskip
\Tweakskip
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{root}
\endgroup
\end{document}