[isabelle-dev] NEWS: formal comments

Lawrence Paulson lp15 at cam.ac.uk
Tue Feb 6 15:13:50 CET 2018

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.


> 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>

More information about the isabelle-dev mailing list