doc-src/TutorialI/tutorial.tex
 author nipkow Mon Oct 09 10:18:21 2000 +0200 (2000-10-09) changeset 10171 59d6633835fa parent 10133 e187dacd248f child 10178 aecb5bf6f76f 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{CTL/ctl}

    69 \input{Advanced/advanced}

    70 %\chapter{The Tricks of the Trade}

    71 \input{appendix}

    72

    73 \bibliographystyle{plain}

    74 \bibliography{../manual}

    75 \printindex

    76 \end{document}