doc-src/TutorialI/tutorial.tex
 author paulson Tue Jul 24 11:25:54 2001 +0200 (2001-07-24) changeset 11450 1b02a6c4032f parent 11428 332347b9b942 child 11456 7eb63f63e6c6 permissions -rw-r--r--
tweaks and indexing
     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{\isacommand{primrec}}}

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

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

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

    18 \index{settings|see{flags}}

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

    20

    21 \underscoreoff

    22

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

    24

    25 \pagestyle{headings}

    26

    27

    28 \begin{document}

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

    30        \\ \vspace{0.5cm} The Tutorial

    31        \\ --- DRAFT ---}

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

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

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

    35 University of Cambridge\\

    36 Computer Laboratory}

    37 \maketitle

    38

    39 \pagenumbering{roman}

    40 \setcounter{page}{5}

    41

    42 \input{preface}

    43

    44 \tableofcontents

    45

    46 \cleardoublepage\pagenumbering{arabic}

    47

    48 \input{basics}

    49 \input{fp}

    50 \input{Rules/rules}

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

    52 \input{Inductive/inductive}

    53 \input{Types/types}

    54 \input{Advanced/advanced}

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

    56 \input{Protocol/protocol}

    57 %\chapter{Structured Proofs}

    58 %\label{ch:Isar}

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

    60 %\chapter{The Tricks of the Trade}

    61 \input{appendix}

    62

    63 \bibliographystyle{plain}

    64 \bibliography{../manual}

    65 \printindex

    66 \end{document}