wneuper/isa: doc-src/TutorialI/tutorial.tex@20e3616b2d9c

     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!

    10 \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)

    11 %\remarksfalse

    13 \makeindex

    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}}

    23 \underscoreoff

    25 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???

    27 \pagestyle{headings}

    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 \pagenumbering{roman}

    43 \maketitle

    44 \newpage

    46 %\setcounter{page}{5}

    47 %\vspace*{\fill}

    48 %\begin{center}

    49 %\LARGE In memoriam \\[1ex]

    50 %{\sc Annette Schumann}\\[1ex]

    51 %1959 -- 2001

    52 %\end{center}

    53 %\vspace*{\fill}

    54 %\vspace*{\fill}

    55 %\newpage

    57 \include{preface}

    59 \tableofcontents

    61 \cleardoublepage\pagenumbering{arabic}

    63 \part{Elementary Techniques}

    64 \include{basics}

    65 \include{fp}

    66 \include{Documents/documents}

    68 \part{Logic and Sets}

    69 \include{Rules/rules}

    70 \include{Sets/sets}

    71 \include{Inductive/inductive}

    73 \part{Advanced Material}

    74 \include{Types/types}

    75 \include{Advanced/advanced}

    76 \include{Protocol/protocol}

    78 \markboth{}{}

    79 \cleardoublepage

    80 \vspace*{\fill}

    81 \begin{flushright}

    82 \begin{tabular}{l}

    83 {\large\sf\slshape You know my methods. Apply them!}\\[1ex]

    84 Sherlock Holmes

    85 \end{tabular}

    86 \end{flushright}

    87 \vspace*{\fill}

    88 \vspace*{\fill}

    90 \underscoreoff

    92 \include{appendix}

    94 \bibliographystyle{plain}

    95 \bibliography{../manual}

    96 \underscoreoff

    97 \printindex

    98 \end{document}

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 30956	9b294296691b
child 43382	bf89455ccf9d
permissions	-rw-r--r--