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



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




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