NEWS

 constant and its defining fact become qualified, e.g. Option.is_none and
 Option.is_none_def. Occasional INCOMPATIBILITY in applications.
 
 * Combinator to represent case distinction on products is named "uncurry",
 with "split" and "prod_case" retained as input abbreviations.
+Partially applied occurences of "uncurry" with eta-contracted body
+terms are not printed with special syntax, to provide a compact
+notation and getting rid of a special-case print translation.
+Hence, the "uncurry"-expressions are printed the following way:
+a) fully applied "uncurry f p": explicit case-expression;
+b) partially applied with explicit double lambda abstraction in
+the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;
+c) partially applied with eta-contracted body term "uncurry f":
+no special syntax, plain "uncurry" combinator.
+This aims for maximum readability in a given subterm.
 INCOMPATIBILITY.
 
 * Some old and rarely used ASCII replacement syntax has been removed.
 INCOMPATIBILITY, standard syntax with symbols should be used instead.
 The subsequent commands help to reproduce the old forms, e.g. to
 simplify porting old theories:
 
   type_notation Map.map  (infixr "~=>" 0)
   notation Map.map_comp  (infixl "o'_m" 55)
+
+* Case combinator "prod_case" with eta-contracted body functions
+has explicit "uncurry" notation, to provide a compact notation while
+getting ride of a special case translation.  Slight syntactic
+INCOMPATIBILITY.
 
 * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
 been removed. INCOMPATIBILITY.
 
 * Quickcheck setup for finite sets.