src/ZF/Constructible/document/root.tex

prefer sign-agnostic conversion following bit structure

\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\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{The Constructible Universe\\ and the\\
       Relative Consistency of the Axiom of Choice}
\author{Lawrence C Paulson}
\maketitle

\begin{abstract}
  G\"odel's proof of the relative consistency of the axiom of
  choice~\cite{goedel40} is one of the most important results in the
  foundations of mathematics. It bears on Hilbert's first problem, namely the
  continuum hypothesis, and indeed G\"odel also proved the relative
  consistency of the continuum hypothesis. Just as important, G\"odel's proof
  introduced the \emph{inner model} method of proving relative consistency,
  and it introduced the concept of \emph{constructible
    set}. Kunen~\cite{kunen80} gives an excellent description of this body of
  work.
  
  This Isabelle/ZF formalization demonstrates G\"odel's claim that his proof
  can be undertaken without using metamathematical arguments, for example
  arguments based on the general syntactic structure of a formula. Isabelle's
  automation replaces the metamathematics, although it does not eliminate the
  requirement at least to state many tedious results that would otherwise be
  unnecessary.
  
  This formalization~\cite{paulson-consistency} is by far the deepest result
  in set theory proved in any automated theorem prover. It rests on a previous
  formal development of the reflection theorem~\cite{paulson-reflection}.
\end{abstract}

\tableofcontents

\begin{center}
  \includegraphics[scale=0.7]{session_graph}
\end{center}

\newpage

\parindent 0pt\parskip 0.5ex

\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}