| changeset 81125 | ec121999a9cb |
| parent 81121 | 7cacedbddba7 |
| child 81133 | 072cc2a92ba3 |
--- 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