这个问题扩展了问题 How to hide defined constants .
我导入理论 A、B 和 C，也许将来还会导入 D、 E, ...
所有的理论都定义了一个函数f。我想在我当前的理论中隐藏 f 的定义，而不改变导入的理论。当我写 term f 时，我得到 A.f。当我将 hide_const (open) f 添加到我当前的理论时，A.f 被隐藏，但现在我得到 B.f 作为 f。如何完全隐藏 f？
我需要像 (hide_const (open) f)+ 这样的东西。
最佳答案
每个理论的函数 f 版本都有不同的名称(A.f、B.f、C.f)，这些都必须单独隐藏。
不过，您可以使用单个 hide_const 命令隐藏多个名称，这是我推荐的:
hide_const (open) A.f B.f C.f
关于isabelle - 如何隐藏多重定义的常量，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/16263203/