45 \begin{document} |
45 \begin{document} |
46 \title{\includegraphics[scale=.8]{isabelle_hol} |
46 \title{\includegraphics[scale=.8]{isabelle_hol} |
47 \\ \vspace{0.5cm} The Tutorial |
47 \\ \vspace{0.5cm} The Tutorial |
48 \\ --- DRAFT ---} |
48 \\ --- DRAFT ---} |
49 \author{Tobias Nipkow\\ |
49 \author{Tobias Nipkow\\ |
50 Technische Universit\"at M\"unchen \\ |
50 Technische Universit{\"a}t M{\"u}nchen \\ |
51 Institut f\"ur Informatik \\ |
51 Institut f{\"u}r Informatik \\ |
52 \url{http://www.in.tum.de/~nipkow/}} |
52 \url{http://www.in.tum.de/~nipkow/}} |
53 \maketitle |
53 \maketitle |
54 |
54 |
55 \pagenumbering{roman} |
55 \pagenumbering{roman} |
56 \tableofcontents |
56 \tableofcontents |
57 |
57 |
58 \subsubsection*{Acknowledgements} |
58 \subsubsection*{Acknowledgements} |
59 This tutorial owes a lot to the constant discussions with and the valuable |
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\"uller, |
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 |
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 |
62 and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to |
63 read and comment on a draft version. |
63 read and comment on a draft version. |
64 \clearfirst |
64 \clearfirst |
65 |
65 |
66 \input{basics} |
66 \input{basics} |
67 \input{fp} |
67 \input{fp} |
68 \input{CTL/ctl} |
68 \chapter{The Rules of the Game} |
|
69 \input{sets} |
|
70 \chapter{Inductively Defined Sets} |
69 \input{Advanced/advanced} |
71 \input{Advanced/advanced} |
|
72 \chapter{More about Types} |
|
73 \chapter{Theory Presentation} |
|
74 \chapter{Case Study: The Needhamd-Schroeder Protocol} |
|
75 \chapter{Structured Proofs} |
|
76 \chapter{Case Study: UNIX File-System Security} |
70 %\chapter{The Tricks of the Trade} |
77 %\chapter{The Tricks of the Trade} |
71 \input{appendix} |
78 \input{appendix} |
72 |
79 |
73 \bibliographystyle{plain} |
80 \bibliographystyle{plain} |
74 \bibliography{../manual} |
81 \bibliography{../manual} |