wneuper/isa: doc-src/TutorialI/tutorial.tex@270b285d48ee

     1 \documentclass{article}

     2 \newif\ifremarks

     3 \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)

     4 \usepackage{cl2emono-modified,isabelle,isabellesym}

     5 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}

     6 \usepackage{../proof,amsmath}

     7 \usepackage{../pdfsetup}    %last package!

     9 %\newtheorem{theorem}{Theorem}[section]

    10 \newtheorem{Exercise}{Exercise}[section]

    11 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}

    12 \newcommand{\ttlbr}{\texttt{[|}}

    13 \newcommand{\ttrbr}{\texttt{|]}}

    14 \newcommand{\ttor}{\texttt{|}}

    15 \newcommand{\ttall}{\texttt{!}}

    16 \newcommand{\ttuniquex}{\texttt{?!}}

    17 \newcommand{\ttEXU}{\texttt{EX!}}

    18 \newcommand{\ttAnd}{\texttt{!!}}

    20 \newcommand{\isasymimp}{\isasymlongrightarrow}

    21 \newcommand{\isasymImp}{\isasymLongrightarrow}

    22 \newcommand{\isasymFun}{\isasymRightarrow}

    23 \newcommand{\isasymuniqex}{\isamath{\exists!\,}}

    25 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}

    27 %% lcp's macros

    28 \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}

    29 \newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules

    30 \let\bigisa=\isa

    31 %% was previously

    32 %% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}}

    33 %% because \isa is too small for variables, but does it really matter?

    36 %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}

    37 %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}

    38 %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}

    39 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}

    40 %% run    ../sedindex logics    to prepare index file

    42 \makeindex

    43 \newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}

    44 \newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}

    45 \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}

    46 \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}

    48 \underscoreoff

    50 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???

    52 \pagestyle{headings}

    53 %\sloppy

    54 %\binperiod     %%%treat . like a binary operator

    56 \begin{document}

    57 \title{\includegraphics[scale=.8]{isabelle_hol}

    58        \\ \vspace{0.5cm} The Tutorial

    59        \\ --- DRAFT ---}

    60 \author{Tobias Nipkow \& Lawrence Paulson\\[1ex]

    61 Technische Universit{\"a}t M{\"u}nchen \\

    62 Institut f{\"u}r Informatik \\[1ex]

    63 University of Cambridge\\

    64 Computer Laboratory}

    65 \maketitle

    67 \pagenumbering{roman}

    68 \tableofcontents

    70 \subsubsection*{Acknowledgements}

    71 This tutorial owes a lot to the constant discussions with and the valuable

    72 feedback from the Isabelle group at Munich: Olaf M{\"u}ller,

    73 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch

    74 and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to

    75 read and comment on a draft version.

    76 \clearfirst

    78 \input{basics}

    79 \input{fp}

    80 \input{Rules/rules}

    81 \input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter

    82 \input{Inductive/inductive}

    83 \input{Advanced/advanced}

    84 \input{Types/types}

    85 \chapter{Theory Presentation}

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

    87 \chapter{Structured Proofs}

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

    89 %\chapter{The Tricks of the Trade}

    90 \input{appendix}

    92 \bibliographystyle{plain}

    93 \bibliography{../manual}

    94 \printindex

    95 \end{document}

author	nipkow
	Mon, 27 Nov 2000 16:40:56 +0100
changeset 10524	270b285d48ee
parent 10522	ed3964d1f1a4
child 10543	8e4307d1207a
permissions	-rw-r--r--