Mixfix annotations may use single-quote-space as documented
- 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. A literal single quote needs to be escaped properly. Minor INCOMPATIBILITY.
This refers to Isabelle/d350aabace23.
Written by makarius on Mar 15 2020, 1:48 PM.