doc-src/TutorialI/tutorial.tex
 author paulson Fri Jul 13 18:22:13 2001 +0200 (2001-07-13) changeset 11423 49312d90cf1f parent 11412 54dd65d0ae87 child 11428 332347b9b942 permissions -rw-r--r--
oops
     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{termination|see{total function}}

    14 \index{product type|see{pair}}

    15 \index{tuple|see{pair}}

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

    17

    18 \underscoreoff

    19

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

    21

    22 \pagestyle{headings}

    23

    24

    25 \begin{document}

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

    27        \\ \vspace{0.5cm} The Tutorial

    28        \\ --- DRAFT ---}

    29 \author{Tobias Nipkow \& Lawrence Paulson\\[1ex]

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

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

    32 University of Cambridge\\

    33 Computer Laboratory}

    34 \maketitle

    35

    36 \pagenumbering{roman}

    37 \setcounter{page}{5}

    38

    39 \input{preface}

    40

    41 \tableofcontents

    42

    43 \newpage\pagenumbering{arabic}

    44

    45 \input{basics}

    46 \input{fp}

    47 \input{Rules/rules}

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

    49 \input{Inductive/inductive}

    50 \input{Types/types}

    51 \input{Advanced/advanced}

    52 %\chapter{Theory Presentation} Document preparation / Syntax Matters!

    53 \input{Protocol/protocol}

    54 %\chapter{Structured Proofs}

    55 %\label{ch:Isar}

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

    57 %\chapter{The Tricks of the Trade}

    58 \input{appendix}

    59

    60 \bibliographystyle{plain}

    61 \bibliography{../manual}

    62 \printindex

    63 \end{document}