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