Email Gateway (Jan 28 2026 at 14:46): Email Gateway (Jan 28 2026 at 14:46):From: Tassilo Lemke <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
not sure if this is the right place to ask, but I haven’t found any concrete answers on this so far. Is there a way to get superscripts and subscripts to align vertically above each other in the generated PDF document? For example, in plain LaTeX, "x^i_j" renders "i" and "j" aligned above/below the same symbol. However, in the generated PDF, they appear sequentially, one after the other.
Since I haven’t found anything on this so far: is this currently not possible, or is it deliberately prevented in order to preserve semantic ordering? In my specific case, the ordering is relevant, although only one ordering results in a well-formed expression (and the correct ordering is also ensured via notation priorities). Still, having them vertically aligned would make the generated PDF much more readable.
Thankful for any suggestions.
Best,
Tassilo Lemke
Email Gateway (Jan 29 2026 at 07:30):From: Tobias Nipkow <nipkow@in.tum.de>
What exactly does your Isabelle term look like? I am asking because it is not
clear to me if i or j are part of the name or if the power operator ^ is
involved or what.
Tobias
On 28/01/2026 15:45, Tassilo Lemke (via cl-isabelle-users Mailing List) wrote:
Hi all,
not sure if this is the right place to ask, but I haven’t found any
concrete answers on this so far. Is there a way to get superscripts and
subscripts to align vertically above each other in the generated PDF document?
For example, in plain LaTeX, "x^i_j" renders "i" and "j" aligned above/below the
same symbol. However, in the generated PDF, they appear sequentially, one after
the other.Since I haven’t found anything on this so far: is this currently not possible,
or is it deliberately prevented in order to preserve semantic ordering? In my
specific case, the ordering is relevant, although only one ordering results in a
well-formed expression (and the correct ordering is also ensured via notation
priorities). Still, having them vertically aligned would make the generated PDF
much more readable.Thankful for any suggestions.
Best,
Tassilo Lemke
Email Gateway (Jan 30 2026 at 00:58):From: Tassilo Lemke <cl-isabelle-users@lists.cam.ac.uk>
To give a bit more context, I am working on a small project regarding social choice and the issue arises when defining the domain, i.e. the allowed preferene profiles of the voters.
Take for example the following definitions:
-- This takes a set of allowed preference relations (W) and allows all preference profiles, where each voter submits a preference relation of W.
-- Practically, this turns a set of allowed preference relations to a set of allowed preference profiles.
definition pp_pow :: "'a rel set ⇒ 'b set ⇒ ('a, 'b) pp set" (‹(_)(⇧_)› [99, 1000] 99) where
"W⇧N ≡ {P. 𝒩⇘P⇙ = N ∧ (∀v∈N. P!v ∈ W)}"
-- This only allows those preference relations of R, which are dichotomous (i.e. voters put alternatives only into one of two categories).
-- Note that this works on a set of allowed preference relations, and not profiles.
definition dom_dich :: "'a rel set ⇒ 'a rel set" (‹(_)⇘DICH⇙› [99] 100) where
"R⇘DICH⇙ ≡ {r∈R. ∀x y z. x ≻⇘r⇙ y ⟶ z ∼⇘r⇙ x ∨ z ∼⇘r⇙ y}"
-- Another domain of interest is restricting a set of profiles to only allow those, whose majority preference relation is transitive.
-- This requires D to be a set of preference profiles, because for the majority relation to be defined, we already need multiple voters.
definition dom_trans :: "('a, 'b) pp set ⇒ ('a, 'b) pp set" (‹(_)⇘TRANS⇙› [99] 100) where
"D⇘TRANS⇙ ≡ {P∈D. trans (majority P)}"
Of course, the ordering in Isabelle itself is relevant, i.e. "(W⇧N)⇘TRANS⇙" and "W⇘DICH⇙⇧N" are well-formed expressions, but "(W⇧N)⇘DICH⇙" and "W⇘TRANS⇙⇧N" are not (W is a set of preference relations). But it would be neat to have both aligned above each other in the generated PDF, as it is always guaranteed to be unambiguous in the context and makes it much more readable.
Best,
Tassilo
Von: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> im Auftrag von Tobias Nipkow <nipkow@in.tum.de>
Gesendet: Donnerstag, 29. Januar 2026 08:29:52
An: cl-isabelle-users@lists.cam.ac.uk
Betreff: Re: [isabelle] Alignment of super- and subscripts in generated PDF output
What exactly does your Isabelle term look like? I am asking because it is not
clear to me if i or j are part of the name or if the power operator ^ is
involved or what.
Tobias
On 28/01/2026 15:45, Tassilo Lemke (via cl-isabelle-users Mailing List) wrote:
Hi all,
not sure if this is the right place to ask, but I haven’t found any
concrete answers on this so far. Is there a way to get superscripts and
subscripts to align vertically above each other in the generated PDF document?
For example, in plain LaTeX, "x^i_j" renders "i" and "j" aligned above/below the
same symbol. However, in the generated PDF, they appear sequentially, one after
the other.Since I haven’t found anything on this so far: is this currently not possible,
or is it deliberately prevented in order to preserve semantic ordering? In my
specific case, the ordering is relevant, although only one ordering results in a
well-formed expression (and the correct ordering is also ensured via notation
priorities). Still, having them vertically aligned would make the generated PDF
much more readable.Thankful for any suggestions.
Best,
Tassilo Lemke
Last updated: Jan 31 2026 at 12:53 UTC