# HG changeset patch
# User nipkow
# Date 1538317415 -7200
# Node ID b96dd4963e2d2b34a975e2eeda3c02d0f6d79628
# Parent  b28ad89d8a50f7282f33a1a9b38cfbca49b0f727
news

diff -r b28ad89d8a50 -r b96dd4963e2d NEWS
--- a/NEWS	Sun Sep 30 13:00:08 2018 +0200
+++ b/NEWS	Sun Sep 30 16:23:35 2018 +0200
@@ -34,15 +34,18 @@
 SUPREMUM, UNION, INTER should now rarely occur in output and are just
 retained as migration auxiliary. INCOMPATIBILITY.
 
-* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
-provers, has been updated.
+* Theory List: the precedence of the list_update operator has changed:
+"f a [n := x]" now needs to be written "(f a)[n := x]".
+
+* Theory "HOL-Library.Multiset": the <Union># operator now has the same
+precedence as any other prefix function symbol.
 
 * Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
 and prod_mset.swap, similarly to sum.swap and prod.swap.
 INCOMPATIBILITY.
 
-* Theory "HOL-Library.Multiset": the <Union># operator now has the same
-precedence as any other prefix function symbol.
+* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
+provers, has been updated.
 
 
 *** ML ***