NEWS

 "fact".  INCOMPATIBILITY: need to name facts explicitly in rare
 situations.
 
 
 *** HOL ***
+
+* Theory Product_Type: duplicated lemmas split_Pair_apply and injective_fst_snd
+removed, use split_eta and prod_eqI instead.  Renamed upd_fst to apfst and upd_snd
+to apsnd.  INCOMPATIBILITY.
 
 * Theory Nat: removed redundant lemmas that merely duplicate lemmas of
 the same name in theory Orderings:
 
   less_trans

 
 * New primrec package.  Specification syntax conforms in style to
 definition/function/....  No separate induction rule is provided.  The
 "primrec" command distinguishes old-style and new-style specifications
 by syntax.  The former primrec package is now named OldPrimrecPackage.
-When adjusting theories, beware: constants stemming for new-style
+When adjusting theories, beware: constants stemming from new-style
 primrec specifications have authentic syntax.
 
 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.
 
 * Library/ListVector: new theory of arithmetic vector operations.

   - Efficient_Nat implements natural numbers by integers, which in general will
     result in higher efficency; pattern matching with 0/Suc is eliminated;
     includes Code_Integer.
   - Code_Index provides an additional datatype index which is mapped to
     target-language built-in integers.
-  - Code_Message provides an additional datatype message_string} which is isomorphic to
+  - Code_Message provides an additional datatype message_string which is isomorphic to
     strings; messages are mapped to target-language strings.
 
 * New package for inductive predicates
 
   An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via