[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