[isabelle-dev] New AFP/devel entry Native_Word

[Tobias Nipkow]

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.

Enjoy!