doc-src/IsarOverview/Isar/document/root.tex

prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);

\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}