[isabelle] find_theorems finds private lemmas
I noticed that the private qualifier does not prevent find_theorems from listing the lemma
when the block has ended. I find this irritating, because there is no way to actually use
the lemma. Indeed, if I try to access it, I get an error "Inaccessible fact".
Why should find_theorems list inaccessible facts at all?
My normal use case is to search for theorems that I want to use right now. Private lemmas
are not usable and merely pollute the search results. What other use cases motivate the
Here is a minimal example:
definition "test = True"
context begin private lemma test: "test" by(simp add: test_def) end
(* found 2 theorem(s):
Scratch.test_def: test â True *)
thm Scratch.test (* error "Inaccessible fact" *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and