[isabelle-dev] NEWS
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Sat Feb 16 08:22:13 CET 2013
* Numeric types mapped by default to target language numerals:
natural (replaces former code_numeral) and integer (replaces
former code_int). Conversions are available as integer_of_natural /
natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and
Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in ML).
INCOMPATIBILITY.
* Discontinued theories Code_Integer and Efficient_Nat by a more
fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
Code_Target_Nat and Code_Target_Numeral. See the tutorial on
code generation for details. INCOMPATIBILITY.
This refers to changeset 310b94ed1815.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130216/f8b3a76a/attachment.asc>
More information about the isabelle-dev
mailing list