Re: [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main
I think I made some changes to the imports during my overhaul of rings.
It had something to do with pending sort hypotheses. In retrospect, a
more ad-hoc solution may have been the better choice considering these
I also think that hiding ii is a reasonable solution (as long as it is
still accessible as Complex.ii or similar) but then the question is what
to do about pi or similarly short names like sin, cos, exp, cis.
This archive was generated by a fusion of
Pipermail (Mailman edition) and