doc-src/TutorialI/tutorial.tex
author wenzelm
Thu Oct 19 21:20:07 2000 +0200 (2000-10-19)
changeset 10272 c02171c5fb20
parent 10236 7626cb4e1407
child 10298 b5fe1ab860fc
permissions -rw-r--r--
tuned \isasymuniqex;
     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}{\isamath{\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}