doc-src/TutorialI/tutorial.tex
 author wenzelm Sun May 01 16:36:34 2011 +0200 (2011-05-01) changeset 42511 bf89455ccf9d parent 30956 9b294296691b child 48171 28a6d67c93f0 permissions -rw-r--r--
eliminated copies of isabelle style files;
 paulson@11423  1 \documentclass{article}  paulson@14400  2 %%\includeonly{Types/types} %%UNCOMMENT to process only selected chapters  wenzelm@42511  3 \usepackage{cl2emono-modified,../../lib/texinputs/isabelle,../../lib/texinputs/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@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 }  haftmann@30956  42 \pagenumbering{roman}  paulson@11423  43 \maketitle  haftmann@30956  44 \newpage  paulson@11423  45 haftmann@30956  46 %\setcounter{page}{5}  nipkow@25257  47 %\vspace*{\fill}  nipkow@25257  48 %\begin{center}  nipkow@25257  49 %\LARGE In memoriam \\[1ex]  nipkow@25257  50 %{\sc Annette Schumann}\\[1ex]  nipkow@25257  51 %1959 -- 2001  nipkow@25257  52 %\end{center}  nipkow@25257  53 %\vspace*{\fill}  nipkow@25257  54 %\vspace*{\fill}  nipkow@25257  55 %\newpage  haftmann@30956  56 paulson@14400  57 \include{preface}  paulson@11423  58 paulson@11423  59 \tableofcontents  paulson@11423  60 paulson@11450  61 \cleardoublepage\pagenumbering{arabic}  paulson@11423  62 wenzelm@12669  63 \part{Elementary Techniques}  paulson@14400  64 \include{basics}  paulson@14400  65 \include{fp}  paulson@14400  66 \include{Documents/documents}  wenzelm@11647  67 wenzelm@11647  68 \part{Logic and Sets}  paulson@14400  69 \include{Rules/rules}  paulson@14400  70 \include{Sets/sets}  paulson@14400  71 \include{Inductive/inductive}  wenzelm@11647  72 wenzelm@11647  73 \part{Advanced Material}  paulson@14400  74 \include{Types/types}  paulson@14400  75 \include{Advanced/advanced}  paulson@14400  76 \include{Protocol/protocol}  wenzelm@11647  77 nipkow@12489  78 \markboth{}{}  nipkow@12489  79 \cleardoublepage  nipkow@12489  80 \vspace*{\fill}  nipkow@12489  81 \begin{flushright}  nipkow@12489  82 \begin{tabular}{l}  nipkow@12489  83 {\large\sf\slshape You know my methods. Apply them!}\\[1ex]  nipkow@12489  84 Sherlock Holmes  nipkow@12489  85 \end{tabular}  nipkow@12489  86 \end{flushright}  nipkow@12489  87 \vspace*{\fill}  nipkow@12489  88 \vspace*{\fill}  nipkow@12489  89 paulson@14400  90 \underscoreoff  paulson@14400  91 paulson@14400  92 \include{appendix}  nipkow@8743  93 nipkow@8743  94 \bibliographystyle{plain}  nipkow@8743  95 \bibliography{../manual}  paulson@14400  96 \underscoreoff  wenzelm@8828  97 \printindex  nipkow@8743  98 \end{document}