| changeset 71545 | b0b16088ccf2 |
| parent 71543 | 317e9ebbc3e1 |
| child 71547 | d350aabace23 |
--- a/NEWS Thu Mar 12 23:05:11 2020 +0100 +++ b/NEWS Fri Mar 13 16:04:27 2020 +0100 @@ -39,6 +39,10 @@ * The inference kernel is now confined to one main module: structure Thm, without the former circular dependency on structure Axclass. +* Mixfix annotations may use "' " (single quote followed by space) to +separate delimiters (as documented in the isar-ref manual), without +requiring an auxiliary empty block. + *** Isar ***