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