11412
|
1 |
\documentclass{article}
\usepackage{cl2emono-modified,isabelle,isabellesym}
\usepackage{../proof,amsmath,amsfonts}
\usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}
\usepackage{../pdfsetup}
%last package!
\remarkstrue %TRUE causes remarks to be displayed (as marginal notes)
%\remarksfalse
\makeindex
\index{termination|see{total function}}
\index{product type|see{pair}}
\index{tuple|see{pair}}
\index{*<*lex*>|see{lexicographic product}}
\underscoreoff
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
\pagestyle{headings}
\begin{document}
\title{\includegraphics[scale=.8]{isabelle_hol}
\\ \vspace{0.5cm} The Tutorial
\\ --- DRAFT ---}
\author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
Technische Universit{\"a}t M{\"u}nchen \\
Institut f{\"u}r Informatik \\[1ex]
University of Cambridge\\
Computer Laboratory}
\maketitle
\pagenumbering{roman}
\setcounter{page}{5}
\input{preface}
\tableofcontents
\newpage\pagenumbering{arabic}
|
8743
|
2 |
\input{basics}
|
|
3 |
\input{fp}
|
10298
|
4 |
\input{Rules/rules}
|
|
5 |
\input{Sets/sets}\input{CTL/ctl} %these constitute ONE chapter
|
10212
|
6 |
\input{Inductive/inductive}
|
10676
|
7 |
\input{Types/types}
|
9958
|
8 |
\input{Advanced/advanced}
|
11207
|
9 |
%\chapter{Theory Presentation} Document preparation / Syntax Matters!
|
11249
|
10 |
\input{Protocol/protocol}
|
11067
|
11 |
%\chapter{Structured Proofs}
|
|
12 |
%\label{ch:Isar}
|
10971
|
13 |
%\chapter{Case Study: UNIX File-System Security}
|
9958
|
14 |
%\chapter{The Tricks of the Trade}
|
8743
|
15 |
\input{appendix}
|
|
16 |
|
|
17 |
\bibliographystyle{plain}
|
|
18 |
\bibliography{../manual}
|
8828
|
19 |
\printindex
|
8743
|
20 |
\end{document}
|