[isabelle] private still pollutes theory namespace
when I use private, e.g. in
theory T imports Main begin
private lemma foo: "..."
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
private lemma foo: "..." *** Duplicate fact declaration
Is this the desired behaviour of "private", or just an imperfect
implementation due to other/technical constraints?
This archive was generated by a fusion of
Pipermail (Mailman edition) and