Re: [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main

Am Donnerstag, den 17.11.2016, 18:17 +0100 schrieb Peter Lammich:
> Hi all,
> I realized that by importing Complex_Main, some very short-named
> constants like "ii" pop up in the global namespace, and thus are not
> available for variable names any more without explicit fixing. This
> is
> very inconvenient. Can't these constants be hidden by default, and
> only
> made visible on demand, eg, as we do for Lattice_Syntax?
> --
> Â Peter
Hm, "ii" (and \<i>) represent the imaginary number, something one can
expect from a theory called Complex_Main.

But as \<i> is also available I think it is okay to hide "ii".

But is this a problem occurring the first time with Isabelle2016-1-
It should be already available in Isabelle2016 (and before).

Â- JohannesÂ

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