doc-src/TutorialI/tutorial.tex
author paulson
Wed Jul 11 13:54:44 2001 +0200 (2001-07-11)
changeset 11402 e143bb9d8255
parent 11389 55e2aef8909b
child 11412 54dd65d0ae87
permissions -rw-r--r--
separate preface and macro file
paulson@10399
     1
\documentclass{article}
paulson@10399
     2
\usepackage{cl2emono-modified,isabelle,isabellesym}
paulson@10597
     3
\usepackage{../proof,amsmath,amsfonts}
paulson@11402
     4
\usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}
wenzelm@8847
     5
\usepackage{../pdfsetup}    %last package!
nipkow@8743
     6
paulson@11402
     7
\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
paulson@11402
     8
%\remarksfalse
nipkow@8743
     9
nipkow@8743
    10
\makeindex
nipkow@8743
    11
nipkow@10654
    12
\index{termination|see{total function}}
nipkow@10543
    13
\index{product type|see{pair}}
nipkow@10543
    14
\index{tuple|see{pair}}
nipkow@10654
    15
\index{*<*lex*>|see{lexicographic product}}
nipkow@10543
    16
nipkow@8743
    17
\underscoreoff
nipkow@8743
    18
nipkow@8743
    19
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
nipkow@8743
    20
nipkow@8743
    21
\pagestyle{headings}
paulson@11402
    22
nipkow@8743
    23
nipkow@8743
    24
\begin{document}
nipkow@8743
    25
\title{\includegraphics[scale=.8]{isabelle_hol}
nipkow@8743
    26
       \\ \vspace{0.5cm} The Tutorial
nipkow@8743
    27
       \\ --- DRAFT ---}
nipkow@10340
    28
\author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
nipkow@10178
    29
Technische Universit{\"a}t M{\"u}nchen \\
nipkow@10340
    30
Institut f{\"u}r Informatik \\[1ex]
nipkow@10340
    31
University of Cambridge\\
nipkow@10340
    32
Computer Laboratory}
nipkow@8743
    33
\maketitle
nipkow@8743
    34
nipkow@8743
    35
\pagenumbering{roman}
paulson@11402
    36
\setcounter{page}{5}
paulson@11402
    37
paulson@11402
    38
\input{preface}
paulson@11402
    39
nipkow@8743
    40
\tableofcontents
nipkow@8743
    41
paulson@11402
    42
\newpage\pagenumbering{arabic}
nipkow@8743
    43
nipkow@8743
    44
\input{basics}
nipkow@8743
    45
\input{fp}
paulson@10298
    46
\input{Rules/rules}
paulson@10298
    47
\input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
nipkow@10212
    48
\input{Inductive/inductive}
nipkow@10676
    49
\input{Types/types}
nipkow@9958
    50
\input{Advanced/advanced}
nipkow@11207
    51
%\chapter{Theory Presentation} Document preparation / Syntax Matters!
paulson@11249
    52
\input{Protocol/protocol}
wenzelm@11067
    53
%\chapter{Structured Proofs}
wenzelm@11067
    54
%\label{ch:Isar}
nipkow@10971
    55
%\chapter{Case Study: UNIX File-System Security}
nipkow@9958
    56
%\chapter{The Tricks of the Trade}
nipkow@8743
    57
\input{appendix}
nipkow@8743
    58
nipkow@8743
    59
\bibliographystyle{plain}
nipkow@8743
    60
\bibliography{../manual}
wenzelm@8828
    61
\printindex
nipkow@8743
    62
\end{document}