[isabelle-dev] Deprecating legacy ASCII symbols?

Lars Noschinski noschinl at in.tum.de
Tue Jun 30 16:28:53 CEST 2015


On 30.06.2015 16:07, Jasmin Blanchette wrote:
> To be complete, I should mention that xsymbols appear in two variants: the backslash-less-than-greater-than variant, the Unicode-like symbol one gets in jEdit. There used to be a third, wrong variant, at least in Proof General: the actual Unicode symbol, which paradoxically didn’t work when copy-pasted back from e.g. an email. (This is no longer an issue?)
In the editor buffer in Isabelle/jEdit, everything is mapped to unicode,
so this is no longer an issue.



More information about the isabelle-dev mailing list