如何让 Isabelle 输出漩涡花饰而不是引号？

Question

多年来，Isabelle 一直在从使用引号

"..."

过渡到使用漩涡花饰

‹...›

来包装类型、对象逻辑术语和符号。截至目前（Isabelle 2023），它仍然相当不一致。

例如，如果我声明一个语言环境：

locale graph = 
  fixes edges :: ‹'s ⇒ 's ⇒ bool› 
    (infix ‹↦› 80)

...Isabelle 输出窗口显示：

locale graph
fixes edges :: "'s ⇒ 's ⇒ bool"  (infix ‹↦› 80)

请注意，类型被包裹在

"..."

中，符号在

‹...›

中。

使用很酷的“草图和探索”功能来生成证明骨架时特别烦人：

[...]
  imports
    "HOL-ex.Sketch_and_Explore"
[...]

lemma ‹reflp (=)›
sketch

--- output ---

proof
  show "(x::'a) = x"
    for x :: 'a
    sorry
qed

现在，漂亮的打印机将术语包装在

"..."

中（并且根本不包装

'a

类型 -_-）。但我想要使用

‹...›

的证明，如果我必须手动更正引号，那么

sketch

的便利性就会受到严重损害。

有什么方法可以告诉 Isabelle/HOL 使用

‹...›

输出所有内容吗？

Answer 1

Isabelle2024 添加了一项将输出设置为漩涡花饰的功能，至少对于大锤和草图探索轮廓：

使用

declare [[atp_proof_cartouches]]

，输出将使用

‹...›

而不是

"..."

进行渲染：

[...]
  imports
    "HOL-ex.Sketch_and_Explore"
[...]

declare [[atp_proof_cartouches]]

lemma ‹reflp (=)›
sketch

--- output ---

proof
  fix x :: 'b
  show ‹x = x›
   sorry
qed

另请注意，轮廓如何更加自然（

fix

而不是

for

）感谢草图和探索的改进。