| author | paulson |
| Wed, 11 Jul 2001 13:54:44 +0200 | |
| changeset 11402 | e143bb9d8255 |
| parent 11389 | 55e2aef8909b |
| child 11412 | 54dd65d0ae87 |
| permissions | -rw-r--r-- |
| paulson@10399 | 1 |
\documentclass{article}
|
| paulson@11402 | 2 |
\usepackage{cl2emono-modified,isabelle,isabellesym}
|
| paulson@11402 | 3 |
\usepackage{../proof,amsmath,amsfonts}
|
| paulson@11402 | 4 |
\usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}
|
| paulson@11402 | 5 |
\usepackage{../pdfsetup} %last package!
|
| paulson@11402 | 6 |
|
| paulson@11389 | 7 |
\remarkstrue %TRUE causes remarks to be displayed (as marginal notes) |
| paulson@11389 | 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}
|