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