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