1

Isabelle/HOL 教程的第 4.1.2 节中,我们发现

按照惯例,只要 Proof General 的 X-Symbol 模式或 LaTeX 输出处于活动状态,就会启用“xsymbols”模式。

现在,随着 Proof General 的衰落,xsymbols 有什么相关性吗?

4

1 回答 1

2

xsymbols模式仍然是 Isabelle/jEdit 中的默认模式。

虽然 Isabelle/jEdit 在编辑器中将符号呈现为 unicode,但在幕后内部表示仍使用xsymbol编码。这可以通过在另一个编辑器中打开保存的理论文件来看到。例如,文本:

lemma "a ∧ b ⟹ b ∧ a"
  by simp

作为其xsymbols编码保存到文件中:

lemma "a \<and> b \<Longrightarrow> b \<and> a"
  by simp

jEdit 的 Isabelle 插件在与主 Isabelle 进程通信时执行与 unicode 之间的转换。Isabelle/etc/symbols(如果您好奇,可以在 中看到翻译表。)

这样做的实际后果是,如果您正在定义符号,xsymbols则指的是所有 LaTeX、ProofGeneral 和 Isabelle/jEdit。

也许将来会有一种unicode模式,取代内部xsymbols表示,但我们还没有。

于 2014-06-20T00:31:11.063 回答