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!
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{!!}}
18 \newcommand{\isasymimp}{\isasymlongrightarrow}
19 \newcommand{\isasymImp}{\isasymLongrightarrow}
20 \newcommand{\isasymFun}{\isasymRightarrow}
21 \newcommand{\isasymuniqex}{\isamath{\exists!\,}}
23 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
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
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}}
39 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
43 %\binperiod %%%treat . like a binary operator
46 \title{\includegraphics[scale=.8]{isabelle_hol}
47 \\ \vspace{0.5cm} The Tutorial
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/}}
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.
68 \chapter{The Rules of the Game}
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}
81 \bibliographystyle{plain}
82 \bibliography{../manual}