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}
8 \remarkstrue %TRUE causes remarks to be displayed (as marginal notes)
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}}
24 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
30 \title{\includegraphics[scale=.8]{isabelle_hol}
31 \\ \vspace{0.5cm} The Tutorial
33 \author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
34 Technische Universit{\"a}t M{\"u}nchen \\
35 Institut f{\"u}r Informatik \\[1ex]
36 University of Cambridge\\
47 \cleardoublepage\pagenumbering{arabic}
52 \input{Sets/sets}\input{CTL/ctl} %these constitute ONE chapter
53 \input{Inductive/inductive}
55 \input{Advanced/advanced}
56 %\chapter{Theory Presentation} Document preparation / Syntax Matters!
57 \input{Protocol/protocol}
58 %\chapter{Structured Proofs}
60 %\chapter{Case Study: UNIX File-System Security}
61 %\chapter{The Tricks of the Trade}
64 \bibliographystyle{plain}
65 \bibliography{../manual}