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