1\documentclass[11pt,a4paper]{article} 2\usepackage{graphicx} 3\usepackage{isabelle,amssymb,isabellesym} 4\usepackage{pdfsetup}\urlstyle{rm} 5 6%table of contents is too crowded! 7\usepackage{tocloft} 8\addtolength\cftsubsecnumwidth {0.5em} 9\addtolength\cftsubsubsecnumwidth {1.0em} 10 11\begin{document} 12 13\title{Equivalents of the Axiom of Choice} 14\author{Krzysztof Gr\c{a}bczewski} 15\maketitle 16 17\begin{abstract} 18 This development~\cite{paulson-gr} proves the equivalence of seven 19 formulations of the well-ordering theorem and twenty formulations of the 20 axiom of choice. It formalizes the first two chapters of the monograph 21 \emph{Equivalents of the Axiom of Choice} by Rubin and 22 Rubin~\cite{rubin&rubin}. Some of this mmaterial involves extremely complex 23 techniques. 24\end{abstract} 25 26\tableofcontents 27 28\begin{center} 29 \includegraphics[width=\textwidth]{session_graph} 30\end{center} 31 32\newpage 33 34\parindent 0pt\parskip 0.5ex 35 36\input{session} 37 38\bibliographystyle{plain} 39\bibliography{root} 40 41\end{document} 42