% The \documentclass ... \xdocumentclass is a hack so that pdflatex can
% be run on the file without doing anything.
\documentclass{article}
\begin{document}
\end{document}
\xdocumentclass
\draft
\input{xref.tex}
% \newcommand{\tlaplustrack}{6}
% \newcommand{\pluscaltrack}{8}
\newcommand{\principlestrack}{7}
%\newcommand{\iospecstrack}{9}
\newcommand{\specificationtrack}{9}
\newcommand{\prooftrack}{10}
\newcommand{\mathtrack}{13}
\newcommand{\topics}{18}
