[isabelle] Specific syntax for identifiers with specific type in LaTeX



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





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