--- a/NEWS Wed Mar 15 15:28:44 2023 +0100
+++ b/NEWS Thu Mar 16 13:37:49 2023 +0100
@@ -52,13 +52,16 @@
Minor INCOMPATIBILITY.
* Theory HOL.Map:
- - Map.empty has been demoted to an input abbreviation only
+ - Map.empty has been demoted to an input abbreviation.
- Map update syntax "_(_ \<mapsto> _)" now has the same priorities
as function update syntax "_(_ := _)". This means:
- 1. "f t(a \<mapsto> b)" becomes "(f t)(a \<mapsto> b)"
- 2. "t(a \<mapsto> b)(c \<mapsto> d)" becomes
+ 1. "f t(a \<mapsto> b)" must now be written "(f t)(a \<mapsto> b)"
+ 2. "t(a \<mapsto> b)(c \<mapsto> d)" must now be written
"t(a \<mapsto> b, c \<mapsto> d)" or
"(t(a \<mapsto> b))(c \<mapsto> d)".
+ Moreover, ":=" and "\<mapsto>" can be mixed freely now.
+ Except in "[...]" maps where ":=" would create a clash with
+ list update syntax "xs[i := x]".
* Theory "HOL.Relation":
- Added predicates irrefl_on and irreflp_on and redefined irrefl and