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 *)

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

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


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