1 |
|
2 % $Id$ |
1 % $Id$ |
3 |
2 |
4 \documentclass[11pt,a4paper]{article} |
3 \documentclass[11pt,a4paper]{article} |
5 \usepackage{graphicx} |
4 \usepackage{graphicx} |
6 \usepackage{isabelle,isabellesym} |
5 \usepackage{isabelle,isabellesym} |
7 \usepackage{amssymb} |
6 \usepackage{amssymb} |
8 \usepackage[latin1]{inputenc} |
7 \usepackage[latin1]{inputenc} |
9 \usepackage[only,bigsqcap]{stmaryrd} |
8 \usepackage[only,bigsqcap]{stmaryrd} |
10 %\usepackage{masmath} |
9 %\usepackage{amsmath} |
11 |
10 |
12 % this should be the last package used |
11 % this should be the last package used |
13 \usepackage{pdfsetup} |
12 \usepackage{pdfsetup} |
14 |
13 |
15 \urlstyle{rm} |
14 \urlstyle{rm} |
16 \isabellestyle{it} |
15 \isabellestyle{tt} |
17 \pagestyle{myheadings} |
16 \pagestyle{myheadings} |
18 |
17 |
19 \begin{document} |
18 \begin{document} |
20 |
19 |
21 \title{The Isabelle/HOL Algebra Library} |
20 \title{The Isabelle/HOL Algebra Library} |
22 \author{ |
21 \author{Clemens Ballarin (Editor)} |
23 Clemens Ballarin \\ |
22 \date{With contributions by Jesús Aransay, Clemens Ballarin, Stephan Hohe, |
24 Florian Kammüller \\ |
23 Florian Kammüller and Lawrence C Paulson \\ |
25 Lawrence C Paulson |
24 \today} |
26 } |
|
27 \maketitle |
25 \maketitle |
28 |
26 |
29 \tableofcontents |
27 \tableofcontents |
30 |
28 |
31 \begin{center} |
29 \begin{center} |
32 \includegraphics[scale=0.5]{session_graph} |
30 \includegraphics[scale=0.5]{session_graph} |
33 \end{center} |
31 \end{center} |
34 |
32 |
35 \clearpage |
33 \clearpage |
36 |
34 |
37 \renewcommand{\isamarkupheader}[1]% |
35 %\renewcommand{\isamarkupheader}[1]% |
38 {\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}} |
36 %{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}} |
39 |
37 |
40 \parindent 0pt\parskip 0.5ex |
38 \parindent 0pt\parskip 0.5ex |
41 \input{session} |
39 \input{session} |
42 |
40 |
43 \pagestyle{headings} |
41 \pagestyle{headings} |