Email Gateway (Nov 26 2020 at 11:28): Email Gateway (Nov 26 2020 at 11:28):From: Tobias Nipkow <nipkow@in.tum.de>
The standard latex output that Isabelle generates for primed identifiers looks
suboptimal: there is too much space between the identifier and the prime. A
possible solution is to replace \isacharprime by \isamath{'}, but one cannot
perform this replacement blindly because type variables like 'a would suffer as
well.
I tried to solve the problem with a new "term style" like (sub) (which turns
trailing digits in identifiers into subscripts) that turns a trailing prime into
"\<^latex>\<open>\\isamath{'}\<close>". However, probably because this is not a
legal variable name (it seems to work for constants) I get the warning
Legacy feature! Bad name binding: "m\<^latex>‹\isamath{'}›"
from @{term "m'"}. I have some vague idea why this gives rise to a "binding"
(probably because free variables are quantified in some manner) but have no idea
how I can avoid this or what other approach to take.
Any suggestions?
Tobias
smime.p7s
Last updated: Jul 15 2022 at 23:21 UTC