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