doc-src/TutorialI/tutorial.tex
 author wenzelm Tue Jan 08 17:32:13 2002 +0100 (2002-01-08) changeset 12669 c1436070c21e parent 12639 71605f976d50 child 12790 8108791e2906 permissions -rw-r--r--
\part{Elementary Techniques};
 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@12669  58 \part{Elementary Techniques}  wenzelm@12669  59 \input{basics}  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}