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: