doc-src/Tutorial/tutorial.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/tutorial.tex	Wed Aug 26 16:57:49 1998 +0200
@@ -0,0 +1,69 @@
+\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}