3

This questions extends the question How to hide defined constants.

I import theory A, B, and C, maybe in future also D, E, ... All theories define a function f. I want to hide the definition of f in my current theory without changing the imported theories. When I write term f I get A.f. When I add hide_const (open) f to my current theory, A.f is hidden but now I get B.f as f. How can I completely hide f? I need something like (hide_const (open) f)+.

4

1 回答 1

5

每个理论的函数版本f都有单独的名称（A.f, B.f, C.f），并且这些都必须单独隐藏。

但是，您可以使用单个hide_const命令隐藏多个名称，这就是我的建议：

hide_const (open) A.f B.f C.f
于 2013-04-28T16:40:16.620 回答