Over the years, Isabelle has been transitioning from using quotes "..." to cartouches ‹...› to wrap types, object logic terms, and notation. As of now (Isabelle 2023), it's still quite inconsistent.
For instance, if I declare a locale:
locale graph =
fixes edges :: ‹'s ⇒ 's ⇒ bool›
(infix ‹↦› 80)
... the Isabelle output window shows:
locale graph
fixes edges :: "'s ⇒ 's ⇒ bool" (infix ‹↦› 80)
Note that the type is wrapped in "...", the notation in ‹...›.
It is particularly annoying when using the cool “sketch and explore” feature to generate proof skeletons:
[...]
imports
"HOL-ex.Sketch_and_Explore"
[...]
lemma ‹reflp (=)›
sketch
--- output ---
proof
show "(x::'a) = x"
for x :: 'a
sorry
qed
Now, the pretty printer wraps the terms in "..." (and does not wrap the 'a type at all -_-). But I want proofs to use ‹...› and the convenience of sketch is severely undermined if I have to correct the quotes by hand.
Is there any way to tell Isabelle/HOL to just output everything using ‹...›?