--- a/NEWS Sun Sep 06 22:14:51 2015 +0200
+++ b/NEWS Sun Sep 06 22:14:51 2015 +0200
@@ -189,6 +189,16 @@
* 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.
@@ -199,6 +209,11 @@
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.