[isabelle-dev] print modes
makarius at sketis.net
Fri May 11 11:21:47 CEST 2012
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.
More information about the isabelle-dev