Email Gateway (Aug 22 2022 at 16:52): Email Gateway (Aug 22 2022 at 16:52):From: Makarius <makarius@sketis.net>
This is controlled by a somewhat older layer in name space management:
Binding.concealed or Name_Space.concealed (in Isabelle/ML).
The included Scratch.thy provides an example for global theory
specifications.
I can't say on the spot if the "concealed" flag should or could become a
qualifier like 'private' / 'qualified'. There is a lot of accumulated
complexity here.
Makarius
Scratch.thy
Email Gateway (Aug 22 2022 at 17:02):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I have a large theory that defines a lot of very technical internal
theorems that are designed to be easily composable from ML and that are
of no interest to an Isabelle user.
I currently mark them as "qualified" to avoid namespace pollution, but
still allow using them from outside e.g. if another theory wants to
extend the tool I'm building. However, there seems to be no way (not
through "private" nor through "hide_fact") to actually stop the theorem
from showing up in "find_theorems".
Is there some way to do this? Would it be desirable to have something
like this (and similarly for definitions)?
Manuel
Last updated: Apr 25 2024 at 16:19 UTC