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,
Concerning applying the patch, I’m not familiar with hg but in git I’dJust 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)
try checking out the commit mentioned in the path, apply it there and
hope for merge to do it’s magic.
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:
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.
Am 12.08.2020 um 17:36 schrieb Pedro Sánchez Terraf <sterraf at famaf.unc.edu.ar>:
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.
El 10/8/20 a las 04:27, Benedikt Nordhoff escribió:
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: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-August/msg00214.html <https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-August/msg00214.html>
Am 28.07.2020 um 15:45 schrieb Pedro Sánchez Terraf <sterraf at famaf.unc.edu.ar> <mailto:sterraf at famaf.unc.edu.ar>:
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?
cs.famaf.unc.edu.ar/~pedro/home_en <https://cs.famaf.unc.edu.ar/~pedro/home_en.html> <https://cs.famaf.unc.edu.ar/~pedro/home_en.html>