Re: [isabelle] private still pollutes theory namespace
> 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" ..
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and