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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
