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 complaints now.

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.

Manuel




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