src/HOL/SET-Protocol/document/root.tex
author paulson
Wed, 04 Jul 2007 13:56:26 +0200
changeset 23563 42f2f90b51a6
parent 14199 d3b8d972a488
permissions -rw-r--r--
simplified a proof
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     1
\documentclass[10pt,a4paper,twoside]{article}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     2
\usepackage{graphicx}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     3
\usepackage{latexsym,theorem}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     4
\usepackage{isabelle,isabellesym}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     5
\usepackage{pdfsetup}\urlstyle{rm}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     6
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     7
\begin{document}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     8
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     9
\pagestyle{headings}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    10
\pagenumbering{arabic}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    11
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    12
\title{Verification of The SET Protocol}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    13
\author{Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson et al.}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    14
\maketitle
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    15
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    16
\tableofcontents
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    17
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    18
\begin{center}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    19
  \includegraphics[scale=0.5]{session_graph}  
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    20
\end{center}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    21
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    22
\newpage
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    23
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    24
\parindent 0pt\parskip 0.5ex
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    25
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    26
\input{session}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    27
\end{document}