src/HOL/Auth/document/root.tex
author wenzelm
Wed, 09 Jun 2004 18:52:42 +0200
changeset 14898 a25550451b51
parent 14734 c5cc02b56e0f
child 17159 d5060118122e
permissions -rw-r--r--
Url.File;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13956
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     1
\documentclass[10pt,a4paper,twoside]{article}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     2
\usepackage{graphicx}
14734
c5cc02b56e0f package needed for superscripts
paulson
parents: 13956
diff changeset
     3
\usepackage[latin1]{inputenc}
13956
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     4
\usepackage{latexsym,theorem}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     5
\usepackage{isabelle,isabellesym}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     6
\usepackage{pdfsetup}\urlstyle{rm}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     7
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     8
\begin{document}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     9
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    10
\pagestyle{headings}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    11
\pagenumbering{arabic}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    12
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    13
\title{Security Protocols}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    14
\author{Giampaolo Bella, Frederic Blanqui, Lawrence C. Paulson et al.}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    15
\maketitle
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    16
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    17
\tableofcontents
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    18
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    19
\begin{center}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    20
  \includegraphics[scale=0.5]{session_graph}  
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    21
\end{center}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    22
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    23
\newpage
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    24
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    25
\parindent 0pt\parskip 0.5ex
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    26
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    27
\input{session}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    28
\end{document}