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}