\documentclass[11pt]{report}

 \usepackage{a4,latexsym}

 \usepackage{graphicx}

 \makeatletter

 \input{../iman.sty}

 \input{extra.sty}

 \makeatother

 \usepackage{ttbox}

 \newcommand\ttbreak{\vskip-10pt\pagebreak[0]}

 %\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=0.2,angle=-90]{isabelle_hol.ps}

        \\ \vspace{0.5cm} The Tutorial

        \\ --- DRAFT ---}

 \author{Tobias Nipkow\\

 Technische Universit\"at M\"unchen \\

 Institut f\"ur Informatik \\

 \texttt{http://www.in.tum.de/\~\relax 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 Merz was also kind enough to read and comment on a

 draft version.

 \clearfirst

 \input{basics}

 \input{fp}

 \input{appendix}

 \bibliographystyle{plain}

 \bibliography{base}

 \input{tutorial.ind}

 \end{document}