doc-src/Tutorial/tutorial.tex
 author nipkow Wed, 26 Aug 1998 16:57:49 +0200 changeset 5375 1463e182c533 child 5376 60b31a24f1a6 permissions -rw-r--r--
The HOL tutorial.

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

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