diff -r 628d87767434 -r 08519594b0e4 doc-src/Tutorial/tutorial.tex
--- a/doc-src/Tutorial/tutorial.tex	Mon Nov 29 11:12:19 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-\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}