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

[Makarius]

On 24/09/18 08:19, Lars Hupel wrote:
>> 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.

OK, thanks.


	Makarius