doc-src/Tutorial/tutorial.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 9677 7808a1ed6daa
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm@7838
     1
\documentclass[11pt,a4paper]{report}
wenzelm@9695
     2
\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,../pdfsetup}
nipkow@5375
     3
nipkow@9255
     4
\newcommand\Out[1]{\texttt{\textsl{#1}}}   %% for output from terminal sessions
nipkow@5375
     5
nipkow@5375
     6
%\newtheorem{theorem}{Theorem}[section]
nipkow@5375
     7
\newtheorem{Exercise}{Exercise}[section]
nipkow@5375
     8
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
nipkow@5375
     9
\newcommand{\ttlbr}{{\tt[|}}
nipkow@5375
    10
\newcommand{\ttrbr}{{\tt|]}}
nipkow@5375
    11
\newcommand{\ttnot}{\tt\~\relax}
nipkow@5375
    12
\newcommand{\ttor}{\tt|}
nipkow@5375
    13
\newcommand{\ttall}{\tt!}
nipkow@5375
    14
\newcommand{\ttuniquex}{\tt?!}
nipkow@5375
    15
nipkow@5375
    16
%% $Id$
nipkow@5375
    17
%%%STILL NEEDS MODAL, LCF
nipkow@5375
    18
%%%\includeonly{ZF}
nipkow@5375
    19
%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
nipkow@5375
    20
%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
nipkow@5375
    21
%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
nipkow@5375
    22
%%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
nipkow@5375
    23
%% run    ../sedindex logics    to prepare index file
nipkow@5375
    24
nipkow@5375
    25
\makeindex
nipkow@5375
    26
nipkow@5375
    27
\underscoreoff
nipkow@5375
    28
nipkow@5375
    29
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
nipkow@5375
    30
nipkow@5375
    31
\pagestyle{headings}
nipkow@5375
    32
%\sloppy
nipkow@5375
    33
%\binperiod     %%%treat . like a binary operator
nipkow@5375
    34
nipkow@5375
    35
\begin{document}
wenzelm@6628
    36
\title{\includegraphics[scale=.8]{isabelle_hol}
nipkow@5375
    37
       \\ \vspace{0.5cm} The Tutorial
nipkow@5375
    38
       \\ --- DRAFT ---}
nipkow@5375
    39
\author{Tobias Nipkow\\
nipkow@5375
    40
Technische Universit\"at M\"unchen \\
nipkow@5375
    41
Institut f\"ur Informatik \\
wenzelm@6628
    42
\url{http://www.in.tum.de/~nipkow/}}
nipkow@5375
    43
\maketitle
nipkow@5375
    44
nipkow@5375
    45
\pagenumbering{roman}
nipkow@5375
    46
\tableofcontents
nipkow@5375
    47
nipkow@5375
    48
\subsubsection*{Acknowledgements}
nipkow@5375
    49
This tutorial owes a lot to the constant discussions with and the valuable
nipkow@5375
    50
feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
nipkow@6099
    51
Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
wenzelm@6584
    52
and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
nipkow@6099
    53
read and comment on a draft version.
nipkow@5375
    54
\clearfirst
nipkow@5375
    55
nipkow@5375
    56
\input{basics}
nipkow@5375
    57
\input{fp}
nipkow@5375
    58
\input{appendix}
nipkow@5375
    59
nipkow@5375
    60
\bibliographystyle{plain}
wenzelm@6603
    61
\bibliography{../manual}
wenzelm@8828
    62
\printindex
nipkow@5375
    63
\end{document}