# HG changeset patch
# User haftmann
# Date 1361095570 -3600
# Node ID bf18bf4922ead40a1345d1a950f1f0cf35829dbb
# Parent  55644f8caeb3c9aa3fba802e2afd6481ea9af299# Parent  35d00ce5862615242458e895758f93ccf13d23db
merged

diff -r 55644f8caeb3 -r bf18bf4922ea NEWS
--- a/NEWS	Sun Feb 17 10:40:53 2013 +0100
+++ b/NEWS	Sun Feb 17 11:06:10 2013 +0100
@@ -6,12 +6,22 @@
 
 *** 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.
+
 * Theory "RealVector" and "Limits": Introduce type class
 (lin)order_topology. Allows to generalize theorems about limits and
 order. Instances are reals and extended reals.
 
-*** HOL ***
-
 * Consolidation of library theories on product orders:
 
     Product_Lattice ~> Product_Order -- pointwise order on products
@@ -170,18 +180,6 @@
 
 *** 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