doc-src/TutorialI/tutorial.tex
 author wenzelm Sat Jan 05 01:19:14 2002 +0100 (2002-01-05) changeset 12639 71605f976d50 parent 12569 e290dadee51c child 12669 c1436070c21e permissions -rw-r--r--
use wasysym package;
 paulson@11423 1 \documentclass{article} paulson@11423 2 \usepackage{cl2emono-modified,isabelle,isabellesym} paulson@11423 3 \usepackage{../proof,amsmath,amsfonts} wenzelm@12639 4 \usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment} wenzelm@12569 5 \let\RightarrowOrig=\Rightarrow\usepackage{marvosym}\let\Rightarrow=\RightarrowOrig %bug in marvosym!? paulson@11423 6 \usepackage{../pdfsetup} paulson@11423 7 %last package! paulson@11423 8 paulson@11423 9 \remarkstrue %TRUE causes remarks to be displayed (as marginal notes) paulson@11423 10 %\remarksfalse paulson@11423 11 paulson@11423 12 \makeindex paulson@11423 13 paulson@11450 14 \index{conditional expressions|see{\isa{if} expressions}} paulson@11456 15 \index{primitive recursion|see{recursion, primitive}} paulson@11428 16 \index{product type|see{pairs and tuples}} paulson@11456 17 \index{structural induction|see{induction, structural}} paulson@11428 18 \index{termination|see{functions, total}} paulson@11428 19 \index{tuples|see{pairs and tuples}} paulson@11428 20 \index{settings|see{flags}} paulson@11423 21 \index{*<*lex*>|see{lexicographic product}} paulson@11423 22 paulson@11423 23 \underscoreoff paulson@11423 24 paulson@11423 25 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? paulson@11423 26 paulson@11423 27 \pagestyle{headings} paulson@11423 28 paulson@11423 29 paulson@11423 30 \begin{document} paulson@11423 31 \title{\includegraphics[scale=.8]{isabelle_hol} paulson@11423 32 \\ \vspace{0.5cm} The Tutorial paulson@11423 33 \\ --- DRAFT ---} paulson@11458 34 \author{Tobias Nipkow and Lawrence C. Paulson\\[1ex] paulson@11423 35 Technische Universit{\"a}t M{\"u}nchen \\ paulson@11423 36 Institut f{\"u}r Informatik \\[1ex] paulson@11423 37 University of Cambridge\\ paulson@11423 38 Computer Laboratory} paulson@11423 39 \maketitle paulson@11423 40 paulson@11423 41 \pagenumbering{roman} paulson@11423 42 \setcounter{page}{5} nipkow@11547 43 \vspace*{\fill} nipkow@11547 44 \begin{center} nipkow@11548 45 \LARGE In memoriam \\[1ex] nipkow@11548 46 {\sc Annette Schumann}\\[1ex] nipkow@11547 47 1959 -- 2001 nipkow@11547 48 \end{center} nipkow@11547 49 \vspace*{\fill} nipkow@11547 50 \vspace*{\fill} nipkow@11547 51 \newpage paulson@11423 52 \input{preface} paulson@11423 53 paulson@11423 54 \tableofcontents paulson@11423 55 paulson@11450 56 \cleardoublepage\pagenumbering{arabic} paulson@11423 57 wenzelm@11647 58 \part{Basic Techniques} %FIXME rename part to "Basic Concepts" (??) wenzelm@11647 59 \input{basics} %FIXME mmw: rename section, move it before part I (??) nipkow@8743 60 \input{fp} wenzelm@11647 61 \input{Documents/documents} wenzelm@11647 62 wenzelm@11647 63 \part{Logic and Sets} paulson@10298 64 \input{Rules/rules} paulson@10298 65 \input{Sets/sets}\input{CTL/ctl} %these constitute ONE chapter nipkow@10212 66 \input{Inductive/inductive} wenzelm@11647 67 wenzelm@11647 68 \part{Advanced Material} nipkow@10676 69 \input{Types/types} nipkow@9958 70 \input{Advanced/advanced} paulson@11249 71 \input{Protocol/protocol} wenzelm@11647 72 nipkow@12489 73 \markboth{}{} nipkow@12489 74 \cleardoublepage nipkow@12489 75 \vspace*{\fill} nipkow@12489 76 \begin{flushright} nipkow@12489 77 \begin{tabular}{l} nipkow@12489 78 {\large\sf\slshape You know my methods. Apply them!}\\[1ex] nipkow@12489 79 Sherlock Holmes nipkow@12489 80 \end{tabular} nipkow@12489 81 \end{flushright} nipkow@12489 82 \vspace*{\fill} nipkow@12489 83 \vspace*{\fill} nipkow@12489 84 nipkow@8743 85 \input{appendix} nipkow@8743 86 nipkow@8743 87 \bibliographystyle{plain} nipkow@8743 88 \bibliography{../manual} wenzelm@8828 89 \printindex nipkow@8743 90 \end{document}