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}