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
paulson@11423
     1
\documentclass{article}
paulson@11423
     2
\usepackage{cl2emono-modified,isabelle,isabellesym}
paulson@11423
     3
\usepackage{../proof,amsmath,amsfonts}
paulson@11423
     4
\usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}
paulson@11423
     5
\usepackage{../pdfsetup}   
paulson@11423
     6
%last package!
paulson@11423
     7
paulson@11423
     8
\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
paulson@11423
     9
%\remarksfalse
paulson@11423
    10
paulson@11423
    11
\makeindex
paulson@11423
    12
paulson@11450
    13
\index{conditional expressions|see{\isa{if} expressions}}
paulson@11428
    14
\index{primitive recursion|see{\isacommand{primrec}}}
paulson@11428
    15
\index{product type|see{pairs and tuples}}
paulson@11428
    16
\index{termination|see{functions, total}}
paulson@11428
    17
\index{tuples|see{pairs and tuples}}
paulson@11428
    18
\index{settings|see{flags}}
paulson@11423
    19
\index{*<*lex*>|see{lexicographic product}}
paulson@11423
    20
paulson@11423
    21
\underscoreoff
paulson@11423
    22
paulson@11423
    23
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
paulson@11423
    24
paulson@11423
    25
\pagestyle{headings}
paulson@11423
    26
paulson@11423
    27
paulson@11423
    28
\begin{document}
paulson@11423
    29
\title{\includegraphics[scale=.8]{isabelle_hol}
paulson@11423
    30
       \\ \vspace{0.5cm} The Tutorial
paulson@11423
    31
       \\ --- DRAFT ---}
paulson@11423
    32
\author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
paulson@11423
    33
Technische Universit{\"a}t M{\"u}nchen \\
paulson@11423
    34
Institut f{\"u}r Informatik \\[1ex]
paulson@11423
    35
University of Cambridge\\
paulson@11423
    36
Computer Laboratory}
paulson@11423
    37
\maketitle
paulson@11423
    38
paulson@11423
    39
\pagenumbering{roman}
paulson@11423
    40
\setcounter{page}{5}
paulson@11423
    41
paulson@11423
    42
\input{preface}
paulson@11423
    43
paulson@11423
    44
\tableofcontents
paulson@11423
    45
paulson@11450
    46
\cleardoublepage\pagenumbering{arabic}
paulson@11423
    47
nipkow@8743
    48
\input{basics}
nipkow@8743
    49
\input{fp}
paulson@10298
    50
\input{Rules/rules}
paulson@10298
    51
\input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
nipkow@10212
    52
\input{Inductive/inductive}
nipkow@10676
    53
\input{Types/types}
nipkow@9958
    54
\input{Advanced/advanced}
nipkow@11207
    55
%\chapter{Theory Presentation} Document preparation / Syntax Matters!
paulson@11249
    56
\input{Protocol/protocol}
wenzelm@11067
    57
%\chapter{Structured Proofs}
wenzelm@11067
    58
%\label{ch:Isar}
nipkow@10971
    59
%\chapter{Case Study: UNIX File-System Security}
nipkow@9958
    60
%\chapter{The Tricks of the Trade}
nipkow@8743
    61
\input{appendix}
nipkow@8743
    62
nipkow@8743
    63
\bibliographystyle{plain}
nipkow@8743
    64
\bibliography{../manual}
wenzelm@8828
    65
\printindex
nipkow@8743
    66
\end{document}