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

     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!

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

    12 %\remarksfalse

    14 \makeindex

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

    24 \underscoreoff

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

    28 \pagestyle{headings}

    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

    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

    58 \include{preface}

    60 \tableofcontents

    62 \cleardoublepage\pagenumbering{arabic}

    64 \part{Elementary Techniques}

    65 \include{basics}

    66 \include{fp}

    67 \include{Documents/documents}

    69 \part{Logic and Sets}

    70 \include{Rules/rules}

    71 \include{Sets/sets}

    72 \include{Inductive/inductive}

    74 \part{Advanced Material}

    75 \include{Types/types}

    76 \include{Advanced/advanced}

    77 \include{Protocol/protocol}

    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}

    91 \underscoreoff

    93 \include{appendix}

    95 \bibliographystyle{plain}

    96 \bibliography{../manual}

    97 \underscoreoff

    98 \printindex

    99 \end{document}

author	wenzelm
	Thu, 26 Jul 2012 19:16:04 +0200
changeset 49540	a33784b07c6b
parent 49537	708278fc2dff
permissions	-rw-r--r--