Isabelle/Pure 中 CONST 的含义是什么？在 HOL.thy 中，我们有以下代码块：
translations "∃!x. P" ⇌ "CONST Ex1 (λx. P)"
translations "THE x. P" ⇌ "CONST The (λx. P)"
translations
"_Let (_binds b bs) e" ⇌ "_Let b (_Let bs e)"
"let x = a in e" ⇌ "CONST Let a (λx. e)"
我试图理解“THE”的含义，并在 HOL.thy 中找到了这个。“THE”在这里有所解释，但我并没有真正了解基本情况，因为假设 P :: 'a ==> a' ==> bool
definition test :: "'a ==> 'a" where
"test y = (THE x. (P x y))"
如果不存在 x st P xy，“test y”如何输入“'a”？不知何故，这必须隐藏在 CONST 和 The 中（我也不太明白，因为它只是公理地给出了类型为 "('a ==> bool) ==> 'a" 的东西，没有任何属性）。
也许最重要的是，在哪里有所有这些的参考？它不在 Isabelle/Isar 参考手册、Isabelle HOL 教程、Isabelle/Isar 实现 pdf、理论文件的评论中，或者我能找到的任何地方。