How to hide defined constants

问题:

When I import theory files which come with defined constants (for recursive functions or definitions) like f, how can I hide such a constant in the current theory file? In other words, I want to make sure that f is a free variable. I do not want to change the imported files.

回答1:

That is exactly the purpose of the hide_const command. E.g.,

hide_const f

will completely remove the defined constant f from the current context (and thus make it inaccessible). If you use

hide_const (open) f

instead, only the base name is hidden (i.e., f), but the qualified name (e.g., A.f if f was defined in theory A) still works.

There are similar commands for classes, types, and facts: hide_class, hide_type, and hide_fact. See also the Isabelle/Isar Reference Manual, page 105.