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" *)
>
> Best,
> Andreas
>
>



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