# 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 # 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 # 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 ***