NEWS

     This outputs a suggestion with instantiations of the facts using the
     "of" attribute (e.g. "assms(1)[of x]").
 
 * Code generator: command 'code_reserved' now uses parentheses for
 target languages, similar to 'code_printing'.
+
+* Theory "HOL.Orderings": Added experimental support for inserting
+additional premises when the order solver is called. This can used to
+e.g. extend the order solver to deal with numerals. In Isabelle/HOL,
+hooks can be added with HOL_Base_Order_Tac.declare_insert_prems_hook.
 
 * Theory "HOL.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
     Minor INCOMPATIBILITY.
   - Renamed lemmas. Minor INCOMPATIBILITY.

 iterated Suc terms.
 
 * Theory "HOL-Library.Adhoc_Overloading" has been moved to Pure. Minor
 INCOMPATIBILITY: need to adjust theory imports.
 
-* Theory "HOL.Orderings":
-  Added experimental support for inserting additional premises when the order solver is called.
-  This can used to e.g. extend the order solver to deal with numerals. 
-  In Isabelle/HOL, hooks can be added with HOL_Base_Order_Tac.declare_insert_prems_hook.
 
 *** ML ***
 
 * Term.variant_bounds replaces former Term.variant_frees for logical
 manipulation of terms, without inner-syntax operations (e.g. reading a