Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Using different symbols in LaTeX

view this post on Zulip Email Gateway (Aug 18 2022 at 12:35):

From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi

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

and

#} 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.

Thanks

Peter

Last updated: May 03 2024 at 08:18 UTC