On 06.02.2018 17:31, Tobias Nipkow wrote:
This concerns only the inner syntax, where comments are rare. We should not give up the outer (* *) comments for something less convenient.

Informal outer comments are not going to disappear.

That means that users who don't have a formal meaning of comments in mind can remain unclear about it as before. (BTW, I often see outer comments in AFP articles that are actually meant as formal 'text' blocks, but apparently the authors never looked at the PDF output, where the informal comments are not shown at all -- just like % in LaTeX.)

isabelle-dev mailing list

Reply via email to