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}