[isabelle-dev] NEWS: discontinued old-style inner comments

[Lars Hupel]

> There were a few remaining uses in AFP. Notable changes are
> AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources
> generated by LEM (!). I don't know how LEM is maintained: it needs to
> produce different inner comments next time, and can actually use
> \<comment> CARTOUCHE notation uniformly for inner and outer comments --
> also note that this needs to be LaTeX-conformant, e.g. by another nested
> cartouche or \<^verbatim>CARTOUCHE.

The way this works is that I'll have to send them a patch. This should
hopefully be simple enough.