doc-src/TutorialI/tutorial.tex
author haftmann
Mon Apr 20 15:24:57 2009 +0200 (2009-04-20)
changeset 30956 9b294296691b
parent 26913 67040326ab7a
child 42511 bf89455ccf9d
permissions -rw-r--r--
empty page leads to results on duplex printers as expected
paulson@11423
     1
\documentclass{article}
paulson@14400
     2
%%\includeonly{Types/types} %%UNCOMMENT to process only selected chapters
wenzelm@26913
     3
\usepackage{cl2emono-modified,../isabelle,../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}