Email Gateway (Aug 22 2022 at 17:34): Email Gateway (Aug 22 2022 at 17:34):From: Makarius <makarius@sketis.net>
On 07/06/18 15:23, Cezary Kaliszyk wrote:
The "―" symbol (even without the cartouche) is no longer available for
user notations in the inner syntax.
Does it mean you've had inner syntax with the \<comment> symbol of
Isabelle? Or syntax with a particular Unicode point (which is generally
fragile)?
What is your application of the special symbol? As there are infinitely
many named Isabelle symbols, we could try to allocate a new one for
Unicode rendering.
term "op ∨" does not parse anymore.
That is "(∨)" in the new notation.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC