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