doc-src/TutorialI/tutorial.tex
author paulson
Fri Aug 03 18:04:55 2001 +0200 (2001-08-03)
changeset 11458 09a6c44a48ea
parent 11456 7eb63f63e6c6
child 11547 bdac4a14b350
permissions -rw-r--r--
numerous stylistic changes 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{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 
    43 \input{preface}
    44 
    45 \tableofcontents
    46 
    47 \cleardoublepage\pagenumbering{arabic}
    48 
    49 \input{basics}
    50 \input{fp}
    51 \input{Rules/rules}
    52 \input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
    53 \input{Inductive/inductive}
    54 \input{Types/types}
    55 \input{Advanced/advanced}
    56 %\chapter{Theory Presentation} Document preparation / Syntax Matters!
    57 \input{Protocol/protocol}
    58 %\chapter{Structured Proofs}
    59 %\label{ch:Isar}
    60 %\chapter{Case Study: UNIX File-System Security}
    61 %\chapter{The Tricks of the Trade}
    62 \input{appendix}
    63 
    64 \bibliographystyle{plain}
    65 \bibliography{../manual}
    66 \printindex
    67 \end{document}