\documentclass[11pt,a4paper]{report}
\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,../pdfsetup}
\newcommand\Out[1]{\texttt{\textsl{#1}}} %% for output from terminal sessions
%\newtheorem{theorem}{Theorem}[section]
\newtheorem{Exercise}{Exercise}[section]
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
\newcommand{\ttlbr}{{\tt[|}}
\newcommand{\ttrbr}{{\tt|]}}
\newcommand{\ttnot}{\tt\~\relax}
\newcommand{\ttor}{\tt|}
\newcommand{\ttall}{\tt!}
\newcommand{\ttuniquex}{\tt?!}
%% $Id$
%%%STILL NEEDS MODAL, LCF
%%%\includeonly{ZF}
%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
%% run ../sedindex logics to prepare index file
\makeindex
\underscoreoff
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
\pagestyle{headings}
%\sloppy
%\binperiod %%%treat . like a binary operator
\begin{document}
\title{\includegraphics[scale=.8]{isabelle_hol}
\\ \vspace{0.5cm} The Tutorial
\\ --- DRAFT ---}
\author{Tobias Nipkow\\
Technische Universit\"at M\"unchen \\
Institut f\"ur Informatik \\
\url{http://www.in.tum.de/~nipkow/}}
\maketitle
\pagenumbering{roman}
\tableofcontents
\subsubsection*{Acknowledgements}
This tutorial owes a lot to the constant discussions with and the valuable
feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
read and comment on a draft version.
\clearfirst
\input{basics}
\input{fp}
\input{appendix}
\bibliographystyle{plain}
\bibliography{../manual}
\printindex
\end{document}