[isabelle-dev] NEWS: formal comments

[Lawrence Paulson]

Will there still be a way to comment out random junk? I often work with a mixture of Isabelle and commented-out HOL Light material.

Larry

> On 26 Jan 2018, at 20:19, Makarius <makarius at sketis.net> wrote:
> 
> * Old-style inner comments (* ... *) within the term language are legacy
> and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"
> instead.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180206/94a61766/attachment-0001.html>