1%
2% Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3%
4% SPDX-License-Identifier: CC-BY-SA-4.0
5%
6
7\documentclass[11pt,a4paper]{article}
8\usepackage{isabelle,isabellesym}
9
10% this should be the last package used
11\usepackage{pdfsetup}
12
13% urls in roman style, theory text in math-similar italics
14\urlstyle{rm}
15\isabellestyle{tt}
16
17
18\begin{document}
19
20\title{Finite Machine Word Library}
21\author{Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski,\\
22       Japheth Lim, Corey Lewis, Daniel Matichuk, Thomas Sewell}
23\maketitle
24
25\begin{abstract}
26  This entry contains an extension to the Isabelle library for fixed-width
27  machine words. In particular, the entry adds quickcheck setup for words,
28  printing as hexadecimals, additional operations, reasoning about alignment,
29  signed words, enumerations of words, normalisation of word numerals, and an
30  extensive library of properties about generic fixed-width words, as well as
31  an instantiation of many of these to the commonly used 32 and 64-bit bases.
32
33  In addition to the listed authors, the entry contains contributions by
34  Nelson Billing, Andrew Boyton, Matthew Brecknell, Cornelius Diekmann,Peter
35  Gammie, Gianpaolo Gioiosa, David Greenaway, Lars Noschinski, Sean Seefried,
36  and Simon Winwood.
37\end{abstract}
38
39\tableofcontents
40
41\parindent 0pt\parskip 0.5ex
42
43% generated text of all theories
44\input{session}
45
46\end{document}
47
48%%% Local Variables:
49%%% mode: latex
50%%% TeX-master: t
51%%% End: