Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Word_Lib/document/   (Sammlung formaler Beweise Version 2026-5©)  Datei vom 29.4.2026 mit Größe 1 kB image not shown  

Quelle  root.tex

  Sprache: Latech
 

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

\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\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, Sascha Böhme, 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
  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}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

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

Messung V0.5 in Prozent
C=97 H=100 G=98

¤ Dauer der Verarbeitung: 0.1 Sekunden  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.