1 \documentclass{article}
3 \remarkstrue %TRUE causes remarks to be displayed (as marginal notes)
4 \usepackage{cl2emono-modified,isabelle,isabellesym}
5 \usepackage{../proof,amsmath,amsfonts}
6 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
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}}
28 \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
29 \newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules
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
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 \index{termination|see{total function}}
49 \index{product type|see{pair}}
50 \index{tuple|see{pair}}
51 \index{*<*lex*>|see{lexicographic product}}
55 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
59 %\binperiod %%%treat . like a binary operator
62 \title{\includegraphics[scale=.8]{isabelle_hol}
63 \\ \vspace{0.5cm} The Tutorial
65 \author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
66 Technische Universit{\"a}t M{\"u}nchen \\
67 Institut f{\"u}r Informatik \\[1ex]
68 University of Cambridge\\
75 \subsubsection*{Acknowledgements}
76 This tutorial owes a lot to the constant discussions with and the valuable
77 feedback from the Isabelle group at Munich: Olaf M{\"u}ller,
78 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
79 and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
80 read and comment on a draft version.
86 \input{Sets/sets}\input{CTL/ctl} %these constitute ONE chapter
87 \input{Inductive/inductive}
89 \input{Advanced/advanced}
90 \chapter{Theory Presentation}
91 \chapter{Case Study: The Needhamd-Schroeder Protocol}
92 \chapter{Structured Proofs}
93 \chapter{Case Study: UNIX File-System Security}
94 %\chapter{The Tricks of the Trade}
97 \bibliographystyle{plain}
98 \bibliography{../manual}