doc-src/TutorialI/tutorial.tex
author paulson
Thu Jul 12 16:36:26 2001 +0200 (2001-07-12)
changeset 11412 54dd65d0ae87
parent 11402 e143bb9d8255
child 11423 49312d90cf1f
permissions -rw-r--r--
more in the Springer style
paulson@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}
nipkow@8743
     2
\input{basics}
nipkow@8743
     3
\input{fp}
paulson@10298
     4
\input{Rules/rules}
paulson@10298
     5
\input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
nipkow@10212
     6
\input{Inductive/inductive}
nipkow@10676
     7
\input{Types/types}
nipkow@9958
     8
\input{Advanced/advanced}
nipkow@11207
     9
%\chapter{Theory Presentation} Document preparation / Syntax Matters!
paulson@11249
    10
\input{Protocol/protocol}
wenzelm@11067
    11
%\chapter{Structured Proofs}
wenzelm@11067
    12
%\label{ch:Isar}
nipkow@10971
    13
%\chapter{Case Study: UNIX File-System Security}
nipkow@9958
    14
%\chapter{The Tricks of the Trade}
nipkow@8743
    15
\input{appendix}
nipkow@8743
    16
nipkow@8743
    17
\bibliographystyle{plain}
nipkow@8743
    18
\bibliography{../manual}
wenzelm@8828
    19
\printindex
nipkow@8743
    20
\end{document}