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}