This concerns only the inner syntax, where comments are rare. We should not give up the outer (* *) comments for something less convenient.


On 06/02/2018 15:13, Lawrence Paulson wrote:
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 < <>> wrote:

* Old-style inner comments (* ... *) within the term language are legacy
and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"

isabelle-dev mailing list

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to