changeset 81135 | d90869a85f60 |
parent 81134 | d23f5a898084 |
child 81139 | d74e53f67474 |
--- a/NEWS Tue Oct 08 22:56:27 2024 +0200 +++ b/NEWS Tue Oct 08 23:31:06 2024 +0200 @@ -75,6 +75,7 @@ unbundle no abs_syntax unbundle no floor_ceiling_syntax unbundle no uminus_syntax + unbundle no funcset_syntax This is more robust than individual 'no_syntax' / 'no_notation' commands, which need to copy mixfix declarations from elsewhere and thus