Re: [isabelle] private still pollutes theory namespace



Dear Peter,

> Is this the desired behaviour of "private", or just an imperfect
> implementation due to other/technical constraints?

I haven't yet looked too closely how "private" works, but the behaviour
appears to be consistent with "hide_fact":

  lemma foo: "True" ..
  hide_fact foo

  thm foo (* error *)
  find_theorems True name: foo (* lists Scratch.foo *)

  lemma foo: "True" .. (* error: duplicate *)

The only difference I found is in the error message produced by "thm foo".

Cheers
Lars




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