src/HOL/Auth/document/root.tex
author wenzelm
Tue, 09 Mar 2021 21:11:05 +0100
changeset 73404 299f6a8faccc
parent 40945 b8703f63bfb2
permissions -rw-r--r--
proper type-setting of cartouches (requires T1); \usepackage[T1]{fontenc} is default for mkroot; \usepackage[utf8]{inputenc} is obsolete in lualatex;
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}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 40945
diff changeset
     2
\usepackage[T1]{fontenc}
13956
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     3
\usepackage{graphicx}
29907
6b9eea61057c fix document generation
huffman
parents: 17159
diff changeset
     4
\usepackage{amssymb}
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 29907
diff changeset
     5
\usepackage{textcomp}
13956
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     6
\usepackage{latexsym,theorem}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     7
\usepackage{isabelle,isabellesym}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     8
\usepackage{pdfsetup}\urlstyle{rm}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
     9
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    10
\begin{document}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    11
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    12
\pagestyle{headings}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    13
\pagenumbering{arabic}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    14
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    15
\title{Security Protocols}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    16
\author{Giampaolo Bella, Frederic Blanqui, Lawrence C. Paulson et al.}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    17
\maketitle
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    18
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    19
\tableofcontents
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    20
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    21
\begin{center}
17159
d5060118122e tuned size of included graph;
wenzelm
parents: 14734
diff changeset
    22
  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
13956
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    23
\end{center}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    24
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    25
\newpage
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    26
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    27
\parindent 0pt\parskip 0.5ex
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    28
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    29
\input{session}
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents:
diff changeset
    30
\end{document}