# HG changeset patch
# User haftmann
# Date 1360999268 -3600
# Node ID 35d00ce5862615242458e895758f93ccf13d23db
# Parent  58f8716b04ee0298dc970ec68f72d94ddc97b646
restored proper order of NEWS entries (lost due too long-waiting patches)

diff -r 58f8716b04ee -r 35d00ce58626 NEWS
--- a/NEWS	Fri Feb 15 16:53:39 2013 +0100
+++ b/NEWS	Sat Feb 16 08:21:08 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