Changed order of prems in finprod_cong. Slight speedup.
\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
\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}