doc-src/TutorialI/tutorial.tex
 author paulson Thu Feb 19 17:57:54 2004 +0100 (2004-02-19) changeset 14400 6069098854b9 parent 13981 70ff42d498c0 child 16359 af7239e3054d permissions -rw-r--r--
new numerics section using type classes
 paulson@11423 1 \documentclass{article} paulson@14400 2 %%\includeonly{Types/types} %%UNCOMMENT to process only selected chapters paulson@11423 3 \usepackage{cl2emono-modified,isabelle,isabellesym} paulson@11423 4 \usepackage{../proof,amsmath,amsfonts} wenzelm@12639 5 \usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment} kleing@13981 6 \usepackage[greek,english]{babel} paulson@11423 7 \usepackage{../pdfsetup} paulson@11423 8 %last package! paulson@11423 9 paulson@11423 10 \remarkstrue %TRUE causes remarks to be displayed (as marginal notes) paulson@11423 11 %\remarksfalse paulson@11423 12 paulson@11423 13 \makeindex paulson@11423 14 paulson@11450 15 \index{conditional expressions|see{\isa{if} expressions}} paulson@11456 16 \index{primitive recursion|see{recursion, primitive}} paulson@11428 17 \index{product type|see{pairs and tuples}} paulson@11456 18 \index{structural induction|see{induction, structural}} paulson@11428 19 \index{termination|see{functions, total}} paulson@11428 20 \index{tuples|see{pairs and tuples}} paulson@11428 21 \index{settings|see{flags}} paulson@11423 22 \index{*<*lex*>|see{lexicographic product}} paulson@11423 23 paulson@11423 24 \underscoreoff paulson@11423 25 paulson@11423 26 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? paulson@11423 27 paulson@11423 28 \pagestyle{headings} paulson@11423 29 paulson@11423 30 paulson@11423 31 \begin{document} nipkow@12790 32 \title{ nipkow@12790 33 \begin{center} nipkow@12790 34 \includegraphics[scale=.8]{isabelle_hol} wenzelm@12916 35 \\ \vspace{0.5cm} A Proof Assistant for Higher-Order Logic nipkow@12790 36 \end{center}} nipkow@12790 37 \author{Tobias Nipkow \quad Lawrence C. Paulson \quad Markus Wenzel%\\[1ex] nipkow@12790 38 %Technische Universit{\"a}t M{\"u}nchen \\ nipkow@12790 39 %Institut f{\"u}r Informatik \\[1ex] nipkow@12790 40 %University of Cambridge\\ nipkow@12790 41 %Computer Laboratory nipkow@12790 42 } paulson@11423 43 \maketitle paulson@11423 44 paulson@11423 45 \pagenumbering{roman} paulson@11423 46 \setcounter{page}{5} nipkow@11547 47 \vspace*{\fill} nipkow@11547 48 \begin{center} nipkow@11548 49 \LARGE In memoriam \\[1ex] nipkow@11548 50 {\sc Annette Schumann}\\[1ex] nipkow@11547 51 1959 -- 2001 nipkow@11547 52 \end{center} nipkow@11547 53 \vspace*{\fill} nipkow@11547 54 \vspace*{\fill} nipkow@11547 55 \newpage paulson@14400 56 \include{preface} paulson@11423 57 paulson@11423 58 \tableofcontents paulson@11423 59 paulson@11450 60 \cleardoublepage\pagenumbering{arabic} paulson@11423 61 wenzelm@12669 62 \part{Elementary Techniques} paulson@14400 63 \include{basics} paulson@14400 64 \include{fp} paulson@14400 65 \include{Documents/documents} wenzelm@11647 66 wenzelm@11647 67 \part{Logic and Sets} paulson@14400 68 \include{Rules/rules} paulson@14400 69 \include{Sets/sets} paulson@14400 70 \include{Inductive/inductive} wenzelm@11647 71 wenzelm@11647 72 \part{Advanced Material} paulson@14400 73 \include{Types/types} paulson@14400 74 \include{Advanced/advanced} paulson@14400 75 \include{Protocol/protocol} wenzelm@11647 76 nipkow@12489 77 \markboth{}{} nipkow@12489 78 \cleardoublepage nipkow@12489 79 \vspace*{\fill} nipkow@12489 80 \begin{flushright} nipkow@12489 81 \begin{tabular}{l} nipkow@12489 82 {\large\sf\slshape You know my methods. Apply them!}\\[1ex] nipkow@12489 83 Sherlock Holmes nipkow@12489 84 \end{tabular} nipkow@12489 85 \end{flushright} nipkow@12489 86 \vspace*{\fill} nipkow@12489 87 \vspace*{\fill} nipkow@12489 88 paulson@14400 89 \underscoreoff paulson@14400 90 paulson@14400 91 \include{appendix} nipkow@8743 92 nipkow@8743 93 \bibliographystyle{plain} nipkow@8743 94 \bibliography{../manual} paulson@14400 95 \underscoreoff wenzelm@8828 96 \printindex nipkow@8743 97 \end{document}