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;
 nipkow@9644  1 % pr(latex xsymbols symbols)  nipkow@8743  2 \documentclass[11pt,a4paper]{report}  wenzelm@8847  3 \usepackage{isabelle,isabellesym}  wenzelm@9695  4 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}  wenzelm@8847  5 \usepackage{../pdfsetup} %last package!  nipkow@8743  6 nipkow@8743  7 %\newtheorem{theorem}{Theorem}[section]  nipkow@8743  8 \newtheorem{Exercise}{Exercise}[section]  nipkow@8743  9 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}  nipkow@8743  10 \newcommand{\ttlbr}{\texttt{[|}}  nipkow@8743  11 \newcommand{\ttrbr}{\texttt{|]}}  nipkow@8743  12 \newcommand{\ttor}{\texttt{|}}  nipkow@8743  13 \newcommand{\ttall}{\texttt{!}}  nipkow@8743  14 \newcommand{\ttuniquex}{\texttt{?!}}  nipkow@8743  15 \newcommand{\ttEXU}{\texttt{EX!}}  nipkow@8743  16 \newcommand{\ttAnd}{\texttt{!!}}  nipkow@8743  17 nipkow@8743  18 \newcommand{\isasymimp}{\isasymlongrightarrow}  nipkow@8743  19 \newcommand{\isasymImp}{\isasymLongrightarrow}  nipkow@8743  20 \newcommand{\isasymFun}{\isasymRightarrow}  wenzelm@10272  21 \newcommand{\isasymuniqex}{\isamath{\exists!\,}}  nipkow@8743  22 nipkow@8743  23 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}  nipkow@8743  24 nipkow@8743  25 %%% to index derived rls: ^$$[a-zA-Z0-9][a-zA-Z0-9_]*$$ \\tdx{\1}  nipkow@8743  26 %%% to index rulenames: ^ *($$[a-zA-Z0-9][a-zA-Z0-9_]*$$, \\tdx{\1}  nipkow@8743  27 %%% to index constants: \\tt $$[a-zA-Z0-9][a-zA-Z0-9_]*$$ \\cdx{\1}  nipkow@8743  28 %%% to deverbify: \\verb|$$[^|]*$$| \\ttindex{\1}  nipkow@8743  29 %% run ../sedindex logics to prepare index file  nipkow@8743  30 nipkow@8743  31 \makeindex  nipkow@8743  32 \newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}  nipkow@8743  33 \newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}  nipkow@8743  34 \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}  nipkow@8743  35 \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}  nipkow@8743  36 nipkow@8743  37 \underscoreoff  nipkow@8743  38 nipkow@8743  39 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???  nipkow@8743  40 nipkow@8743  41 \pagestyle{headings}  nipkow@8743  42 %\sloppy  nipkow@8743  43 %\binperiod %%%treat . like a binary operator  nipkow@8743  44 nipkow@8743  45 \begin{document}  nipkow@8743  46 \title{\includegraphics[scale=.8]{isabelle_hol}  nipkow@8743  47  \\ \vspace{0.5cm} The Tutorial  nipkow@8743  48  \\ --- DRAFT ---}  nipkow@8743  49 \author{Tobias Nipkow\\  nipkow@10178  50 Technische Universit{\"a}t M{\"u}nchen \\  nipkow@10178  51 Institut f{\"u}r Informatik \\  nipkow@8743  52 \url{http://www.in.tum.de/~nipkow/}}  nipkow@8743  53 \maketitle  nipkow@8743  54 nipkow@8743  55 \pagenumbering{roman}  nipkow@8743  56 \tableofcontents  nipkow@8743  57 nipkow@8743  58 \subsubsection*{Acknowledgements}  nipkow@8743  59 This tutorial owes a lot to the constant discussions with and the valuable  nipkow@10178  60 feedback from Larry Paulson and the Isabelle group at Munich: Olaf M{\"u}ller,  nipkow@8743  61 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch  nipkow@8743  62 and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to  nipkow@8743  63 read and comment on a draft version.  nipkow@8743  64 \clearfirst  nipkow@8743  65 nipkow@8743  66 \input{basics}  nipkow@8743  67 \input{fp}  nipkow@10178  68 \chapter{The Rules of the Game}  nipkow@10236  69 \label{ch:Rules}  nipkow@10178  70 \input{sets}  nipkow@10212  71 \input{Inductive/inductive}  nipkow@9958  72 \input{Advanced/advanced}  nipkow@10178  73 \chapter{More about Types}  nipkow@10178  74 \chapter{Theory Presentation}  nipkow@10178  75 \chapter{Case Study: The Needhamd-Schroeder Protocol}  nipkow@10178  76 \chapter{Structured Proofs}  nipkow@10178  77 \chapter{Case Study: UNIX File-System Security}  nipkow@9958  78 %\chapter{The Tricks of the Trade}  nipkow@8743  79 \input{appendix}  nipkow@8743  80 nipkow@8743  81 \bibliographystyle{plain}  nipkow@8743  82 \bibliography{../manual}  wenzelm@8828  83 \printindex  nipkow@8743  84 \end{document}