doc-src/TutorialI/tutorial.tex
author wenzelm
Tue May 09 16:05:45 2000 +0200 (2000-05-09)
changeset 8847 d6c92979fa51
parent 8828 5be2d1745c61
child 9016 d61c76716984
permissions -rw-r--r--
use proper version of pdfsetup.sty;
     1 
     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}