[isabelle-dev] print modes

Christian Sternagel c-sterna at jaist.ac.jp
Fri May 11 11:33:24 CEST 2012

You are right. However, if the "target" is a "newbie", it is often very 
important to have it _exactly_ as it has to be typed (which does not 
necessarily hold depending on syntax translations etc., even if the 
print mode is "").

On 05/11/2012 06:21 PM, Makarius wrote:
> 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

More information about the isabelle-dev mailing list