doc-src/TutorialI/tutorial.tex
author wenzelm
Thu Dec 20 21:13:22 2001 +0100 (2001-12-20)
changeset 12569 e290dadee51c
parent 12489 c92e38c3cbaa
child 12639 71605f976d50
permissions -rw-r--r--
\usepackage{marvosym};
     1 \documentclass{article}
     2 \usepackage{cl2emono-modified,isabelle,isabellesym}
     3 \usepackage{../proof,amsmath,amsfonts}
     4 \usepackage{latexsym,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}