[isabelle-dev] NEWS: update_cartouches
Makarius
makarius at sketis.net
Wed Oct 8 00:25:31 CEST 2014
*** 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
----------------------------------------------------------------------------
More information about the isabelle-dev
mailing list