Mixfix annotations may use single-quote-space as documented
General
- 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.
- Projects
- None
- Subscribers
- None