doc-src/TutorialI/tutorial.tex
author nipkow
Thu Sep 14 17:46:00 2000 +0200 (2000-09-14)
changeset 9958 67f2920862c7
parent 9742 98d3ca2c18f7
child 10133 e187dacd248f
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{Advanced/advanced}
    69 %\chapter{The Tricks of the Trade}
    70 \input{appendix}
    71 
    72 \bibliographystyle{plain}
    73 \bibliography{../manual}
    74 \printindex
    75 \end{document}