doc-src/TutorialI/tutorial.tex
 author nipkow Fri Aug 18 10:34:08 2000 +0200 (2000-08-18) changeset 9644 6b0b6b471855 parent 9016 d61c76716984 child 9677 7808a1ed6daa 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,comment}

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

     6

     7 \usepackage{ttbox}

     8 \newcommand\ttbreak{\vskip-10pt\pagebreak[0]}

     9 \newcommand\Out[1]{\texttt{\textsl{#1}}}   %% for output from terminal sessions

    10

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

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

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

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

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

    16 \newcommand{\ttor}{\texttt{|}}

    17 \newcommand{\ttall}{\texttt{!}}

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

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

    20 \newcommand{\ttAnd}{\texttt{!!}}

    21

    22 \newcommand{\isasymimp}{\isasymlongrightarrow}

    23 \newcommand{\isasymImp}{\isasymLongrightarrow}

    24 \newcommand{\isasymFun}{\isasymRightarrow}

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

    26

    27 \newenvironment{isabellepar}%

    28 {\par\medskip\noindent\begin{isabelle}}{\end{isabelle}\medskip\par\noindent}

    29

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

    31

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

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

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

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

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

    37

    38 \makeindex

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

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

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

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

    43

    44 \underscoreoff

    45

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

    47

    48 \pagestyle{headings}

    49 %\sloppy

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

    51

    52 \begin{document}

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

    54        \\ \vspace{0.5cm} The Tutorial

    55        \\ --- DRAFT ---}

    56 \author{Tobias Nipkow\\

    57 Technische Universit\"at M\"unchen \\

    58 Institut f\"ur Informatik \\

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

    60 \maketitle

    61

    62 \pagenumbering{roman}

    63 \tableofcontents

    64

    65 \subsubsection*{Acknowledgements}

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

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

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

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

    70 read and comment on a draft version.

    71 \clearfirst

    72

    73 \input{basics}

    74 \input{fp}

    75 \input{appendix}

    76

    77 \bibliographystyle{plain}

    78 \bibliography{../manual}

    79 \printindex

    80 \end{document}