[isabelle] private still pollutes theory namespace



Hi,

when I use private, e.g. in 
  theory T imports Main begin
  context begin 
    private lemma foo: "..."
  end

after the context, 
the lemma foo is still visible to find_theorems (as T.foo). 
Moreover, I cannot name any other lemma in theory T foo, even not a
second private one:
  lemma foo: "..." *** Duplicate fact declaration

  context begin
    private lemma foo: "..." *** Duplicate fact declaration


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


--
  Peter






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