[isabelle-dev] @ML antiquotation in generated code

Johannes Hölzl hoelzl at in.tum.de
Thu Oct 9 11:09:20 CEST 2014

In 3094b0edd6b5 I needed to change a document comment {* ..*} to a
source comment (* .. *). Looks like using the @{ML ..} antiquotation in
a document comment does not work. Latex does not allow \verb inside

Is it possible to change \verb to \texttt, with the necessary _ -> \_
and maybe more conversions?

 - Johannes

More information about the isabelle-dev mailing list