[isabelle] find_theorems finds private lemmas



Dear all,

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 current behaviour?

Here is a minimal example:

definition "test = True"
context begin private lemma test: "test" by(simp add: test_def) end
find_theorems test
  (* found 2 theorem(s):
       Scratch.test: test
       Scratch.test_def: test â True *)
thm Scratch.test (* error "Inaccessible fact" *)

Best,
Andreas




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