How to hide certain constants

Question

When I import theory files that have certain 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 modify the imported files.

Answer 1

That is the purpose of the hide_const . For instance.

 hide_const f 

completely removes a certain constant f from the current context (and thus makes it inaccessible). If you use

 hide_const (open) f 

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

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