--- a/NEWS Fri Feb 15 08:31:30 2013 +0100
+++ b/NEWS Fri Feb 15 08:31:31 2013 +0100
@@ -170,6 +170,18 @@
*** HOL ***
+* 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.
+
* Sledgehammer:
- Added MaSh relevance filter based on machine-learning; see the