diff -r 6ce0c8d59f5a -r ec121999a9cb NEWS --- a/NEWS Sun Oct 06 22:56:07 2024 +0200 +++ b/NEWS Tue Oct 08 12:10:35 2024 +0200 @@ -69,6 +69,9 @@ unbundle no rtrancl_syntax unbundle no trancl_syntax unbundle no reflcl_syntax + unbundle no abs_syntax + unbundle no floor_ceiling_syntax + unbundle no uminus_syntax This is more robust than individual 'no_syntax' / 'no_notation' commands, which need to copy mixfix declarations from elsewhere and thus