Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Ctrl+click on notation with sub- and superscri...

Email Gateway (Nov 13 2025 at 08:38):

From: Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

I believe ctrl+click is not working with notation using sub- and
superscripts defined with bsub, esub, bsup, esup. Below are some
examples. I am using the latest Isabelle development version (db80ee4abed1).

Is there anything I can do to make ctrl+click work in such cases?

Best wishes,

Kevin

theory Scratch
   imports Main
begin

definition "bar x ≡ True"
notation bar (‹_⇘bar⇙›)

definition "foo x y ≡ True"
notation foo (infix ‹⊣⇘foo⇙› 50)

(*ctrl+click not working on either term*)
term "x⇘bar⇙"
term "x ⊣⇘foo⇙ y"
term "(⊣⇘foo⇙)"

end

Last updated: Dec 02 2025 at 16:32 UTC