Re: [isabelle] Some Isabelle 2018-RC0 Observations



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.