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;
     1 \documentclass{article}

     2 \usepackage{cl2emono-modified,isabelle,isabellesym}

     3 \usepackage{../proof,amsmath,amsfonts}

     4 \usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment}

     5 \let\RightarrowOrig=\Rightarrow\usepackage{marvosym}\let\Rightarrow=\RightarrowOrig  %bug in marvosym!?

     6 \usepackage{../pdfsetup}

     7 %last package!

     8

     9 \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)

    10 %\remarksfalse

    11

    12 \makeindex

    13

    14 \index{conditional expressions|see{\isa{if} expressions}}

    15 \index{primitive recursion|see{recursion, primitive}}

    16 \index{product type|see{pairs and tuples}}

    17 \index{structural induction|see{induction, structural}}

    18 \index{termination|see{functions, total}}

    19 \index{tuples|see{pairs and tuples}}

    20 \index{settings|see{flags}}

    21 \index{*<*lex*>|see{lexicographic product}}

    22

    23 \underscoreoff

    24

    25 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???

    26

    27 \pagestyle{headings}

    28

    29

    30 \begin{document}

    31 \title{\includegraphics[scale=.8]{isabelle_hol}

    32        \\ \vspace{0.5cm} The Tutorial

    33        \\ --- DRAFT ---}

    34 \author{Tobias Nipkow and Lawrence C. Paulson\\[1ex]

    35 Technische Universit{\"a}t M{\"u}nchen \\

    36 Institut f{\"u}r Informatik \\[1ex]

    37 University of Cambridge\\

    38 Computer Laboratory}

    39 \maketitle

    40

    41 \pagenumbering{roman}

    42 \setcounter{page}{5}

    43 \vspace*{\fill}

    44 \begin{center}

    45 \LARGE In memoriam \\[1ex]

    46 {\sc Annette Schumann}\\[1ex]

    47 1959 -- 2001

    48 \end{center}

    49 \vspace*{\fill}

    50 \vspace*{\fill}

    51 \newpage

    52 \input{preface}

    53

    54 \tableofcontents

    55

    56 \cleardoublepage\pagenumbering{arabic}

    57

    58 \part{Basic Techniques}  %FIXME rename part to "Basic Concepts" (??)

    59 \input{basics}  %FIXME mmw: rename section, move it before part I (??)

    60 \input{fp}

    61 \input{Documents/documents}

    62

    63 \part{Logic and Sets}

    64 \input{Rules/rules}

    65 \input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter

    66 \input{Inductive/inductive}

    67

    68 \part{Advanced Material}

    69 \input{Types/types}

    70 \input{Advanced/advanced}

    71 \input{Protocol/protocol}

    72

    73 \markboth{}{}

    74 \cleardoublepage

    75 \vspace*{\fill}

    76 \begin{flushright}

    77 \begin{tabular}{l}

    78 {\large\sf\slshape You know my methods. Apply them!}\\[1ex]

    79 Sherlock Holmes

    80 \end{tabular}

    81 \end{flushright}

    82 \vspace*{\fill}

    83 \vspace*{\fill}

    84

    85 \input{appendix}

    86

    87 \bibliographystyle{plain}

    88 \bibliography{../manual}

    89 \printindex

    90 \end{document}