1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Tutorial/tutorial.tex	Wed Aug 26 16:57:49 1998 +0200
     1.3 @@ -0,0 +1,69 @@
     1.4 +\documentclass[11pt]{report}
     1.5 +\usepackage{a4,latexsym}
     1.6 +\usepackage{graphicx}
     1.7 +
     1.8 +\makeatletter
     1.9 +\input{../iman.sty}
    1.10 +\input{extra.sty}
    1.11 +\makeatother
    1.12 +\usepackage{ttbox}
    1.13 +\newcommand\ttbreak{\vskip-10pt\pagebreak[0]}
    1.14 +
    1.15 +%\newtheorem{theorem}{Theorem}[section]
    1.16 +\newtheorem{Exercise}{Exercise}[section]
    1.17 +\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
    1.18 +\newcommand{\ttlbr}{{\tt[|}}
    1.19 +\newcommand{\ttrbr}{{\tt|]}}
    1.20 +\newcommand{\ttnot}{\tt\~\relax}
    1.21 +\newcommand{\ttor}{\tt|}
    1.22 +\newcommand{\ttall}{\tt!}
    1.23 +\newcommand{\ttuniquex}{\tt?!}
    1.24 +
    1.25 +%% $Id$
    1.26 +%%%STILL NEEDS MODAL, LCF
    1.27 +%%%\includeonly{ZF}
    1.28 +%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    1.29 +%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
    1.30 +%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
    1.31 +%%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
    1.32 +%% run    ../sedindex logics    to prepare index file
    1.33 +
    1.34 +\makeindex
    1.35 +
    1.36 +\underscoreoff
    1.37 +
    1.38 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    1.39 +
    1.40 +\pagestyle{headings}
    1.41 +%\sloppy
    1.42 +%\binperiod     %%%treat . like a binary operator
    1.43 +
    1.44 +\begin{document}
    1.45 +\title{\includegraphics[scale=0.2,angle=-90]{isabelle_hol.ps}
    1.46 +       \\ \vspace{0.5cm} The Tutorial
    1.47 +       \\ --- DRAFT ---}
    1.48 +\author{Tobias Nipkow\\
    1.49 +Technische Universit\"at M\"unchen \\
    1.50 +Institut f\"ur Informatik \\
    1.51 +\texttt{http://www.in.tum.de/\~\relax nipkow/}}
    1.52 +\maketitle
    1.53 +
    1.54 +\pagenumbering{roman}
    1.55 +\tableofcontents
    1.56 +
    1.57 +\subsubsection*{Acknowledgements}
    1.58 +This tutorial owes a lot to the constant discussions with and the valuable
    1.59 +feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
    1.60 +Wolfgang Naraschewski, David von Oheimb, Leonor Prensa-Nieto, Cornelia Pusch
    1.61 +and Markus Wenzel. Stefan Merz was also kind enough to read and comment on a
    1.62 +draft version.
    1.63 +\clearfirst
    1.64 +
    1.65 +\input{basics}
    1.66 +\input{fp}
    1.67 +\input{appendix}
    1.68 +
    1.69 +\bibliographystyle{plain}
    1.70 +\bibliography{base}
    1.71 +\input{tutorial.ind}
    1.72 +\end{document}