HomeIsabelle/Phabricator
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.

Written by makarius on Mar 15 2020, 1:48 PM.
User
Projects
None
Subscribers
None

Event Timeline