Re: [isabelle] Commenting out inside text <> block



On 18/11/2018 14:11, Peter Lammich wrote:
> 
> Note that LaTeX's % or begin{comment} do not prevent Isabelle from
> processing antiquotations, which may fail, or even interfere, in
> particular with the end-of-line comment %.

You can put everything into a default cartouche (antiquotation with the
name "cartouche"). Thus the body is typeset like formal text, e.g. term
language. Putting a Latex comment before it should be able to suppress
the output.

E.g. like this:

  %‹foo bar \rubbish @{junk›


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.