这个问题扩展了如何隐藏定义的常量的问题。
我进口的理论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