By default, anything from a file is exported and therefore available to
any file importing or using it (except the flags values!). However, you can
make some theorems of rules local using the Local prefix (see
the index of commands).
However, constants and axioms are always exported, and a definition appearing
in an exported definition or theorem is always exported. So it is only useful
to declare local some rules (created using new_intro, new_elim or new_equation), LaTeX syntaxes (created using tex_syntax),
lemmas or definitions only appearing in local lemmas.