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