wneuper/isa: doc-src/TutorialI/tutorial.tex@54dd65d0ae87

     1 \documentclass{article}

     2 \usepackage{cl2emono-modified,isabelle,isabellesym}

     3 \usepackage{../proof,amsmath,amsfonts}

     4 \usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}

     5 \usepackage{../pdfsetup}

     6 %last package!

     8 \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)

     9 %\remarksfalse

    11 \makeindex

    13 \index{termination|see{total function}}

    14 \index{product type|see{pair}}

    15 \index{tuple|see{pair}}

    16 \index{*<*lex*>|see{lexicographic product}}

    18 \underscoreoff

    20 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???

    22 \pagestyle{headings}

    25 \begin{document}

    26 \title{\includegraphics[scale=.8]{isabelle_hol}

    27        \\ \vspace{0.5cm} The Tutorial

    28        \\ --- DRAFT ---}

    29 \author{Tobias Nipkow \& Lawrence Paulson\\[1ex]

    30 Technische Universit{\"a}t M{\"u}nchen \\

    31 Institut f{\"u}r Informatik \\[1ex]

    32 University of Cambridge\\

    33 Computer Laboratory}

    34 \maketitle

    36 \pagenumbering{roman}

    37 \setcounter{page}{5}

    39 \input{preface}

    41 \tableofcontents

    43 \newpage\pagenumbering{arabic}

    44 \input{basics}

    45 \input{fp}

    46 \input{Rules/rules}

    47 \input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter

    48 \input{Inductive/inductive}

    49 \input{Types/types}

    50 \input{Advanced/advanced}

    51 %\chapter{Theory Presentation} Document preparation / Syntax Matters!

    52 \input{Protocol/protocol}

    53 %\chapter{Structured Proofs}

    54 %\label{ch:Isar}

    55 %\chapter{Case Study: UNIX File-System Security}

    56 %\chapter{The Tricks of the Trade}

    57 \input{appendix}

    59 \bibliographystyle{plain}

    60 \bibliography{../manual}

    61 \printindex

    62 \end{document}

author	paulson
	Thu, 12 Jul 2001 16:36:26 +0200
changeset 11412	54dd65d0ae87
parent 11402	e143bb9d8255
child 11423	49312d90cf1f
permissions	-rw-r--r--