doc-src/TutorialI/tutorial.tex
 author nipkow Wed Aug 30 14:38:48 2000 +0200 (2000-08-30) changeset 9742 98d3ca2c18f7 parent 9723 a977245dfc8a child 9958 67f2920862c7 permissions -rw-r--r--
*** empty log message ***
     1 % pr(latex xsymbols symbols)

     2 \documentclass[11pt,a4paper]{report}

     3 \usepackage{isabelle,isabellesym}

     4 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}

     5 \usepackage{../pdfsetup}    %last package!

     6

     7 %\newtheorem{theorem}{Theorem}[section]

     8 \newtheorem{Exercise}{Exercise}[section]

     9 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}

    10 \newcommand{\ttlbr}{\texttt{[|}}

    11 \newcommand{\ttrbr}{\texttt{|]}}

    12 \newcommand{\ttor}{\texttt{|}}

    13 \newcommand{\ttall}{\texttt{!}}

    14 \newcommand{\ttuniquex}{\texttt{?!}}

    15 \newcommand{\ttEXU}{\texttt{EX!}}

    16 \newcommand{\ttAnd}{\texttt{!!}}

    17

    18 \newcommand{\isasymimp}{\isasymlongrightarrow}

    19 \newcommand{\isasymImp}{\isasymLongrightarrow}

    20 \newcommand{\isasymFun}{\isasymRightarrow}

    21 \newcommand{\isasymuniqex}{\emph{$\exists!\,$}}

    22

    23 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}

    24

    25 %%% to index derived rls:  ^$$[a-zA-Z0-9][a-zA-Z0-9_]*$$        \\tdx{\1}

    26 %%% to index rulenames:   ^ *($$[a-zA-Z0-9][a-zA-Z0-9_]*$$,     \\tdx{\1}

    27 %%% to index constants:   \\tt $$[a-zA-Z0-9][a-zA-Z0-9_]*$$     \\cdx{\1}

    28 %%% to deverbify:         \\verb|$$[^|]*$$|     \\ttindex{\1}

    29 %% run    ../sedindex logics    to prepare index file

    30

    31 \makeindex

    32 \newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}

    33 \newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}

    34 \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}

    35 \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}

    36

    37 \underscoreoff

    38

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

    40

    41 \pagestyle{headings}

    42 %\sloppy

    43 %\binperiod     %%%treat . like a binary operator

    44

    45 \begin{document}

    46 \title{\includegraphics[scale=.8]{isabelle_hol}

    47        \\ \vspace{0.5cm} The Tutorial

    48        \\ --- DRAFT ---}

    49 \author{Tobias Nipkow\\

    50 Technische Universit\"at M\"unchen \\

    51 Institut f\"ur Informatik \\

    52 \url{http://www.in.tum.de/~nipkow/}}

    53 \maketitle

    54

    55 \pagenumbering{roman}

    56 \tableofcontents

    57

    58 \subsubsection*{Acknowledgements}

    59 This tutorial owes a lot to the constant discussions with and the valuable

    60 feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,

    61 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch

    62 and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to

    63 read and comment on a draft version.

    64 \clearfirst

    65

    66 \input{basics}

    67 \input{fp}

    68 \input{tricks}

    69 \input{appendix}

    70

    71 \bibliographystyle{plain}

    72 \bibliography{../manual}

    73 \printindex

    74 \end{document}