doc-src/TutorialI/tutorial.tex
 author wenzelm Thu Feb 21 18:19:34 2002 +0100 (2002-02-21) changeset 12916 4ac388e02b74 parent 12790 8108791e2906 child 13981 70ff42d498c0 permissions -rw-r--r--
updated title;
 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} nipkow@12790 31 \title{ nipkow@12790 32 \begin{center} nipkow@12790 33 \includegraphics[scale=.8]{isabelle_hol} wenzelm@12916 34 \\ \vspace{0.5cm} A Proof Assistant for Higher-Order Logic nipkow@12790 35 \end{center}} nipkow@12790 36 \author{Tobias Nipkow \quad Lawrence C. Paulson \quad Markus Wenzel%\\[1ex] nipkow@12790 37 %Technische Universit{\"a}t M{\"u}nchen \\ nipkow@12790 38 %Institut f{\"u}r Informatik \\[1ex] nipkow@12790 39 %University of Cambridge\\ nipkow@12790 40 %Computer Laboratory nipkow@12790 41 } paulson@11423 42 \maketitle paulson@11423 43 paulson@11423 44 \pagenumbering{roman} paulson@11423 45 \setcounter{page}{5} nipkow@11547 46 \vspace*{\fill} nipkow@11547 47 \begin{center} nipkow@11548 48 \LARGE In memoriam \\[1ex] nipkow@11548 49 {\sc Annette Schumann}\\[1ex] nipkow@11547 50 1959 -- 2001 nipkow@11547 51 \end{center} nipkow@11547 52 \vspace*{\fill} nipkow@11547 53 \vspace*{\fill} nipkow@11547 54 \newpage paulson@11423 55 \input{preface} paulson@11423 56 paulson@11423 57 \tableofcontents paulson@11423 58 paulson@11450 59 \cleardoublepage\pagenumbering{arabic} paulson@11423 60 wenzelm@12669 61 \part{Elementary Techniques} wenzelm@12669 62 \input{basics} nipkow@8743 63 \input{fp} wenzelm@11647 64 \input{Documents/documents} wenzelm@11647 65 wenzelm@11647 66 \part{Logic and Sets} paulson@10298 67 \input{Rules/rules} paulson@10298 68 \input{Sets/sets}\input{CTL/ctl} %these constitute ONE chapter nipkow@10212 69 \input{Inductive/inductive} wenzelm@11647 70 wenzelm@11647 71 \part{Advanced Material} nipkow@10676 72 \input{Types/types} nipkow@9958 73 \input{Advanced/advanced} paulson@11249 74 \input{Protocol/protocol} wenzelm@11647 75 nipkow@12489 76 \markboth{}{} nipkow@12489 77 \cleardoublepage nipkow@12489 78 \vspace*{\fill} nipkow@12489 79 \begin{flushright} nipkow@12489 80 \begin{tabular}{l} nipkow@12489 81 {\large\sf\slshape You know my methods. Apply them!}\\[1ex] nipkow@12489 82 Sherlock Holmes nipkow@12489 83 \end{tabular} nipkow@12489 84 \end{flushright} nipkow@12489 85 \vspace*{\fill} nipkow@12489 86 \vspace*{\fill} nipkow@12489 87 nipkow@8743 88 \input{appendix} nipkow@8743 89 nipkow@8743 90 \bibliographystyle{plain} nipkow@8743 91 \bibliography{../manual} wenzelm@8828 92 \printindex nipkow@8743 93 \end{document}