doc-src/TutorialI/tutorial.tex
author wenzelm
Sat Jan 05 01:19:14 2002 +0100 (2002-01-05)
changeset 12639 71605f976d50
parent 12569 e290dadee51c
child 12669 c1436070c21e
permissions -rw-r--r--
use wasysym package;
paulson@11423
     1
\documentclass{article}
paulson@11423
     2
\usepackage{cl2emono-modified,isabelle,isabellesym}
paulson@11423
     3
\usepackage{../proof,amsmath,amsfonts}
wenzelm@12639
     4
\usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment}
wenzelm@12569
     5
\let\RightarrowOrig=\Rightarrow\usepackage{marvosym}\let\Rightarrow=\RightarrowOrig  %bug in marvosym!?
paulson@11423
     6
\usepackage{../pdfsetup}   
paulson@11423
     7
%last package!
paulson@11423
     8
paulson@11423
     9
\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
paulson@11423
    10
%\remarksfalse
paulson@11423
    11
paulson@11423
    12
\makeindex
paulson@11423
    13
paulson@11450
    14
\index{conditional expressions|see{\isa{if} expressions}}
paulson@11456
    15
\index{primitive recursion|see{recursion, primitive}}
paulson@11428
    16
\index{product type|see{pairs and tuples}}
paulson@11456
    17
\index{structural induction|see{induction, structural}}
paulson@11428
    18
\index{termination|see{functions, total}}
paulson@11428
    19
\index{tuples|see{pairs and tuples}}
paulson@11428
    20
\index{settings|see{flags}}
paulson@11423
    21
\index{*<*lex*>|see{lexicographic product}}
paulson@11423
    22
paulson@11423
    23
\underscoreoff
paulson@11423
    24
paulson@11423
    25
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
paulson@11423
    26
paulson@11423
    27
\pagestyle{headings}
paulson@11423
    28
paulson@11423
    29
paulson@11423
    30
\begin{document}
paulson@11423
    31
\title{\includegraphics[scale=.8]{isabelle_hol}
paulson@11423
    32
       \\ \vspace{0.5cm} The Tutorial
paulson@11423
    33
       \\ --- DRAFT ---}
paulson@11458
    34
\author{Tobias Nipkow and Lawrence C. Paulson\\[1ex]
paulson@11423
    35
Technische Universit{\"a}t M{\"u}nchen \\
paulson@11423
    36
Institut f{\"u}r Informatik \\[1ex]
paulson@11423
    37
University of Cambridge\\
paulson@11423
    38
Computer Laboratory}
paulson@11423
    39
\maketitle
paulson@11423
    40
paulson@11423
    41
\pagenumbering{roman}
paulson@11423
    42
\setcounter{page}{5}
nipkow@11547
    43
\vspace*{\fill}
nipkow@11547
    44
\begin{center}
nipkow@11548
    45
\LARGE In memoriam \\[1ex]
nipkow@11548
    46
{\sc Annette Schumann}\\[1ex]
nipkow@11547
    47
1959 -- 2001
nipkow@11547
    48
\end{center}
nipkow@11547
    49
\vspace*{\fill}
nipkow@11547
    50
\vspace*{\fill}
nipkow@11547
    51
\newpage
paulson@11423
    52
\input{preface}
paulson@11423
    53
paulson@11423
    54
\tableofcontents
paulson@11423
    55
paulson@11450
    56
\cleardoublepage\pagenumbering{arabic}
paulson@11423
    57
wenzelm@11647
    58
\part{Basic Techniques}  %FIXME rename part to "Basic Concepts" (??)
wenzelm@11647
    59
\input{basics}  %FIXME mmw: rename section, move it before part I (??)
nipkow@8743
    60
\input{fp}
wenzelm@11647
    61
\input{Documents/documents}
wenzelm@11647
    62
wenzelm@11647
    63
\part{Logic and Sets}
paulson@10298
    64
\input{Rules/rules}
paulson@10298
    65
\input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
nipkow@10212
    66
\input{Inductive/inductive}
wenzelm@11647
    67
wenzelm@11647
    68
\part{Advanced Material}
nipkow@10676
    69
\input{Types/types}
nipkow@9958
    70
\input{Advanced/advanced}
paulson@11249
    71
\input{Protocol/protocol}
wenzelm@11647
    72
nipkow@12489
    73
\markboth{}{}
nipkow@12489
    74
\cleardoublepage
nipkow@12489
    75
\vspace*{\fill}
nipkow@12489
    76
\begin{flushright}
nipkow@12489
    77
\begin{tabular}{l}
nipkow@12489
    78
{\large\sf\slshape You know my methods. Apply them!}\\[1ex]
nipkow@12489
    79
Sherlock Holmes
nipkow@12489
    80
\end{tabular}
nipkow@12489
    81
\end{flushright}
nipkow@12489
    82
\vspace*{\fill}
nipkow@12489
    83
\vspace*{\fill}
nipkow@12489
    84
nipkow@8743
    85
\input{appendix}
nipkow@8743
    86
nipkow@8743
    87
\bibliographystyle{plain}
nipkow@8743
    88
\bibliography{../manual}
wenzelm@8828
    89
\printindex
nipkow@8743
    90
\end{document}