Re: [isabelle] find_theorems finds private lemmas
Em segunda-feira, 16 de novembro de 2015, Andreas Lochbihler <
andreas.lochbihler at inf.ethz.ch> escreveu:
> 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" *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and