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