On Fri, 11 May 2012, Christian Sternagel wrote:
Anyway, what are your remaining applications for ASCII notation?
Currently only, copy-pasting examples from jedit into e-mails for the
Isabelle mailing list ;). Not very convincing, is it?
I think most people now copy the Unicode from the physical rendering seen
in the editor buffer or HTML view. This works most of the time. Formal
text that is copy-pasted is approximative anyway, in the sense that it
lacks the precise context.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
