%
% Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
%
% SPDX-License-Identifier: CC-BY-SA-4.0
%

\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{tt}


\begin{document}

\title{Finite Machine Word Library}
\author{Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski,\\
       Japheth Lim, Corey Lewis, Daniel Matichuk, Thomas Sewell}
\maketitle

\begin{abstract}
  This entry contains an extension to the Isabelle library for fixed-width
  machine words. In particular, the entry adds quickcheck setup for words,
  printing as hexadecimals, additional operations, reasoning about alignment,
  signed words, enumerations of words, normalisation of word numerals, and an
  extensive library of properties about generic fixed-width words, as well as
  an instantiation of many of these to the commonly used 32 and 64-bit bases.

  In addition to the listed authors, the entry contains contributions by
  Nelson Billing, Andrew Boyton, Matthew Brecknell, Cornelius Diekmann,Peter
  Gammie, Gianpaolo Gioiosa, David Greenaway, Lars Noschinski, Sean Seefried,
  and Simon Winwood.
\end{abstract}

\tableofcontents

\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: