Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Specific syntax for identifiers with specific ...

Email Gateway (Aug 18 2022 at 12:51):

From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Dear all,

I would like to have all variable identifiers of a specific type that
occur in @{term ...} and @{thm ...} antiquotations inside text {* ... *}
protions to be decorated in the generated LaTeX output with e.g. hats,
wiggles or the like. The idea is to make it obvious at the first glance
whether a variable is of that specific type or not. Can this be somehow
done automatically for all these antiquotations?

My naive approach would be to declare free constants of this type with
appropriate syntax for the latex output and instantiate all variables of
this type in @{thm ...} antiquotations with such constants and use them
in @{term ...} expressions, too. However, this is very tedious and
error-prone.

Thanks in advance,
Andreas

Last updated: May 03 2024 at 08:18 UTC