Re: [isabelle] Superscript argument to a function

Dear Mikhail,

I've been successfully using your patch on Isabelle2020. Though I tried hard, I couldn't make it work for the current development version (I only managed to make it work with non-nested scripts). Would you mind giving me some hints on how to adapt it?

I'm about to present a formalization to other mathematicians and a smooth notation is key.

Thank you very much in advance,

Pedro Sánchez Terraf
CIEM-FAMAF — Universidad Nacional de Córdoba
On 18/8/20 19:51, Mikhail Mandrykin wrote:

Concerning applying the patch, I’m not familiar with hg but in git I’d
try checking out the commit mentioned in the path, apply it there and
hope for merge to do it’s magic.
Just in case I adapted the patch for Isabelle 2020 (last relevant commit 97ccf48c2f0c) and it works for me on some non-trivial theories with nested subscripts and superscripts (I also don't have any previous experience with Isabelle/Scala though)

Sample original theory source fragment:
also from Sucinner have
    "... = - G κ⇘i+1⇙ κ⇘i+2⇙
           + int (∑x|x<m⇘κ⇘i+1⇙⇙∧x⇧♮∈vars K⇘κ⇘i+1⇙⇙.
                    MAX⇩0 t∈terms K⇘κ⇘i+1⇙⇙|t~P⇘κ⇘i+2⇙⇙!0. #⇘x⇧♮⇙ t * size (σ⇘i+1⇙ x⇧♮))
           - int (∑x≤(m⇘κ⇘i+1⇙⇙ - 1)⇧♯. #⇩x (P⇘κ⇘i+1⇙⇙!0) * size (σ⇘i+1⇙ x))"
    (is "_ + int (∑x∈?S. ?g x) - _ = _ + int (∑x∈?T. ?h x)- _") by


Benedikt Nordhoff писал 2020-08-13 14:33:
Dear Pedro,

I’m certainly not the most qualified to answer this. I haven’t build
Isabelle from source for quite a while. I think back then I used the
README_REPOSITORY file as a guide.

Best Benedikt

Am 12.08.2020 um 17:36 schrieb Pedro Sánchez Terraf <sterraf at>:

Dear Benedikt,

Sorry to bother you with an dumb question, but I do not know how to build jEdit. Could you point me to some docs where I can find this? (Note: I'm not a computer scientist but I can manage some stuff).
It seems that there have been many some movements and the patch should be applied somewhere in

but I could be wrong.

Best wishes,
PST.- <>

El 10/8/20 a las 04:27, Benedikt Nordhoff escribió:
Dear Pedro,

I implemented basic support for this for Isabelle 2014 but it never made it into any release. It worked fine till the 2017 release, I haven’t tried the patch on later versions. If you’re interested and want to try whether the patch still works you can find it here: <>


Am 28.07.2020 um 15:45 schrieb Pedro Sánchez Terraf <sterraf at> <mailto:sterraf at>:

Good day,

I have a question concerning the use of superscripts as arguments to functions. I have a function ccc_rel that has 3 arguments, and I would like that the syntax for the first one is a superscript. (I'm working in ZF, don't know if that is relevant.)

If I enter

    notation ccc_rel (‹ccc⇧_'(_,_')›)

everything works fine *until* the first argument has more than one character. If I use \<bsup>...\<esup> instead:

    notation ccc_rel (‹ccc⇗_⇖'(_,_')›)

it accepts a multi-character first argument but it the PIDE does not prettyprints the superscript.

Can I have the cake and eat it?

PST.- <> <>

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