* 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
