[isabelle-dev] NEWS: formal comments
makarius at sketis.net
Tue Feb 6 18:12:05 CET 2018
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.)
More information about the isabelle-dev