[isabelle-dev] New AFP/devel entry Native_Word

Tobias Nipkow nipkow at in.tum.de
Thu Sep 19 11:09:38 CEST 2013

For users of the development version of the AFP only:

Native Word
Andreas Lochbihler

This entry makes machine words and machine arithmetic available for code
generation from Isabelle/HOL.  It provides a common abstraction that hides the
differences between the different target languages.  The code generator maps
these operations to the APIs of the target languages.  Apart from that, we
extend the available bit operations on types int and integer, and map them to
the operations in the target languages.


More information about the isabelle-dev mailing list