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