如何配置Isabelle使其输出cartouches而非引号？

针对Isabelle在引号与cartouches使用上的不一致问题，有两种可行的解决方式：

全局配置（Isabelle/jEdit） #

通过修改Isabelle的打印选项，可让所有会话默认使用cartouches：

1. 打开Isabelle/jEdit，依次点击 Plugins > Isabelle > Options
2. 切换到Printing标签页
3. 找到并勾选Cartouche quotes for terms/types选项
4. 重启当前Isabelle会话，设置即可生效

局部配置（单个理论文件） #

如果只想让特定理论文件使用cartouches，可在文件开头添加以下配置声明：

declare [[cartouche_quotes = true]]

该设置仅对当前理论文件及导入它的文件生效，不会影响全局环境。

效果验证 #

启用配置后，使用"sketch and explore"生成的证明框架会统一用cartouches包裹术语和类型，示例输出如下：

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

需要注意的是，该配置在Isabelle 2023版本中已支持，部分老旧工具或插件可能存在少量兼容性问题，但核心的sketch功能可正常适配。

内容的提问来源于stack exchange，提问作者Ben Keks