src/ZF/AC/document/root.tex

more accurate goal context;
actually check assertions;

\documentclass[11pt,a4paper]{article}
\usepackage{graphicx}
\usepackage{isabelle,amssymb,isabellesym}
\usepackage{pdfsetup}\urlstyle{rm}

%table of contents is too crowded!
\usepackage{tocloft}
\addtolength\cftsubsecnumwidth {0.5em}
\addtolength\cftsubsubsecnumwidth {1.0em}

\begin{document}

\title{Equivalents of the Axiom of Choice}
\author{Krzysztof Gr\c{a}bczewski}
\maketitle

\begin{abstract}
  This development~\cite{paulson-gr} proves the equivalence of seven
  formulations of the well-ordering theorem and twenty formulations of the
  axiom of choice. It formalizes the first two chapters of the monograph
  \emph{Equivalents of the Axiom of Choice} by Rubin and
  Rubin~\cite{rubin&rubin}. Some of this mmaterial involves extremely complex
  techniques.
\end{abstract}

\tableofcontents

\begin{center}
  \includegraphics[width=\textwidth]{session_graph}
\end{center}

\newpage

\parindent 0pt\parskip 0.5ex

\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}