[isabelle-dev] NEWS: formal comments

[Makarius Wenzel]

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


	Makarius