[isabelle] Using different symbols in LaTeX


I wish to use a different symbol (from stmaryrd.sty) to replace the multiset notation

{# #}

when I build a theory file to output a pdf. However, I only want to do this in the final LaTeXed version of the file. How do I go about telling the isatool-LaTeX compiler to interpret

{# as \Lbag


#} as \Rbag?

I'd also like to specify

{#} as \emptyset or \Lbag \Rbag

but I don't know if this last one would cause problems owing to an overlap with the first one.

I've looked through the document mark-up section, but the method of addressing the problem there was by redefining the syntax in Isabelle. I don't really want to do this, unless it is necessary.



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