[isabelle] Hiding facts from find_theorems



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.