[isabelle-dev] NEWS: update_cartouches

[Tobias Nipkow]

I have no opinion wrt PG but just don't let your update tool lose on the whole 
distribution because there are some files of mine where that would create 
discrepancies in the text.

Tobias

On 08/10/2014 00:25, Makarius wrote:
> *** System ***
>
> * The Isabelle tool "update_cartouches" changes theory files to use cartouches
> instead of old-style {* verbatim *} or `alt_string` tokens.
>
> This refers to Isabelle/fffdbce036db.  In the subsequent changesets, I have
> modernized a few of my own hotspots accordingly, but refrained from large-scale
> updates of theory sources.
>
> The tool emerged from the observation that a few people have already started to
> use cartouches even in main HOL.
>
> It should be noted that Proof General cannot step through such files, so it
> needs to general plan how to proceed.  Is now the time to delete Proof General
> and the TTY loop?
>
>
>      Makarius
>
> ----------------------------------------------------------------------------
>                                http://stop-ttip.org
> ----------------------------------------------------------------------------
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141009/de8c7295/attachment.bin>