replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
\documentclass[envcountsame]{llncs}
%\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}
%for best-style documents ...
\urlstyle{rm}
%\isabellestyle{it}
\newcommand{\tweakskip}{\vspace{-\medskipamount}}
\pagestyle{plain}
\begin{document}
\title{%A Compact Introduction to
Structured Proofs in Isar/HOL\thanks{Published in TYPES 2002, LNCS 2646.}}
\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}
\small
\paragraph{Acknowledgement}
I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer,
Markus Wenzel and Freek Wiedijk commented on and improved this paper.
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{root}
\endgroup
\end{document}