moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
\documentclass[envcountsame]{llncs}
%\documentclass[11pt,a4paper]{article}
\usepackage{../../../../lib/texinputs/isabelle,../../../../lib/texinputs/isabellesym,../../../pdfsetup}
%for best-style documents ...
\urlstyle{rm}
%\isabellestyle{it}
\newcommand{\tweakskip}{\vspace{-\medskipamount}}
\pagestyle{plain}
\begin{document}
\title{A Tutorial Introduction to Structured Isar Proofs}
\author{Tobias Nipkow}
\institute{Institut f{\"u}r Informatik, TU M{\"u}nchen\\
{\small\url{http://www.in.tum.de/~nipkow/}}}
\date{}
\maketitle
\input{intro.tex}
\input{Logic.tex}
\input{Induction.tex}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{root}
\endgroup
\end{document}