[isabelle-dev] NEWS: mixfix annotations and Unicode
makarius at sketis.net
Sat Apr 2 16:28:30 CEST 2016
On Sat, 2 Apr 2016, Makarius wrote:
> I am considering to force Isabelle/jEdit text into Unicode
> non-conformance, to make logical sense. Or we could disallow Unicode
> notation altogether -- it is hardly ever used, apart from some exotic
> A similar problem will show up again, if/when Unicode is supported in
> HOL string literals.
I have made bidirectional Unicode display a bit more robust in
Isabelle/ce22e5c3d4ce. If this sufficient is unclear; the Unicode standard
is vast and complex.
Details about bidirectional text display are in Annex #9:
Anybody wants to formalize this?
More information about the isabelle-dev