doc-src/TutorialI/tutorial.tex
 author wenzelm Mon Oct 01 14:44:00 2001 +0200 (2001-10-01) changeset 11647 0538cb0f7999 parent 11548 0028bd06a19c child 12489 c92e38c3cbaa permissions -rw-r--r--
initial setup for chapter on document preparation;
     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 %\chapter{Structured Proofs}

    73 %\label{ch:Isar}

    74 %\chapter{Case Study: UNIX File-System Security}

    75 %\chapter{The Tricks of the Trade}

    76 \input{appendix}

    77

    78 \bibliographystyle{plain}

    79 \bibliography{../manual}

    80 \printindex

    81 \end{document}