src/HOL/SET_Protocol/document/root.tex
author nipkow
Tue, 17 Jun 2025 14:11:40 +0200
changeset 82733 8b537e1af2ec
parent 73404 299f6a8faccc
permissions -rw-r--r--
reinstated intersection of lists as inter_list_set
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}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 33028
diff changeset
     2
\usepackage[T1]{fontenc}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     3
\usepackage{graphicx}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     4
\usepackage{latexsym,theorem}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     5
\usepackage{isabelle,isabellesym}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     6
\usepackage{pdfsetup}\urlstyle{rm}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     7
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     8
\begin{document}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     9
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    10
\pagestyle{headings}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    11
\pagenumbering{arabic}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    12
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    13
\title{Verification of The SET Protocol}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    14
\author{Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson et al.}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    15
\maketitle
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    16
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    17
\tableofcontents
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    18
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    19
\begin{center}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    20
  \includegraphics[scale=0.5]{session_graph}  
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    21
\end{center}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    22
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    23
\newpage
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    24
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    25
\parindent 0pt\parskip 0.5ex
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    26
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    27
\input{session}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    28
\end{document}