How to hide defined constants
isabelle
Solution
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.
Problem
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.