doc-src/TutorialI/tutorial.tex
 author nipkow Tue Oct 17 13:28:57 2000 +0200 (2000-10-17) changeset 10236 7626cb4e1407 parent 10212 33fe2d701ddd child 10272 c02171c5fb20 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{\"a}t M{\"u}nchen \\

    51 Institut f{\"u}r 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{\"u}ller,

    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 \chapter{The Rules of the Game}

    69 \label{ch:Rules}

    70 \input{sets}

    71 \input{Inductive/inductive}

    72 \input{Advanced/advanced}

    73 \chapter{More about Types}

    74 \chapter{Theory Presentation}

    75 \chapter{Case Study: The Needhamd-Schroeder Protocol}

    76 \chapter{Structured Proofs}

    77 \chapter{Case Study: UNIX File-System Security}

    78 %\chapter{The Tricks of the Trade}

    79 \input{appendix}

    80

    81 \bibliographystyle{plain}

    82 \bibliography{../manual}

    83 \printindex

    84 \end{document}