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