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



On 18/11/16 21:17, Peter Lammich wrote:
> 
> Can you push this please?
> 
> @Makarius: Will this make it into Isabelle2016-1?

A push on isabelle-dev would mean it is for the next release after
Isabelle2016-1. It needs to go to the isabelle-release instead: all
changes need to be sent to me via email. See now
https://bitbucket.org/isabelle_project/isabelle-release/commits/eace715f4988


Here is also the point in history where the slightly odd const name "ii"
was originally introduced, oddly together with the same "ii" as notation:
http://isabelle.in.tum.de/repos/isabelle/rev/10dbf16be15f#l8.17

Here the notation was changed to the current \<i>, without changing the
const name: http://isabelle.in.tum.de/repos/isabelle/rev/67a628beb981#l3.25


Facts are usually just called i_foo_bar instead of ii_foo_bar. So an
obvious reform after the Isabelle2016-1 release is this:

  * rename const "ii" to "imaginary_unit" (with existing syntax \<i>);
    the const name hardly ever shows up in applications

  * standardize all corresponding fact names towards i_foo_bar

In principle, the const could be also called \<i> and the syntax
removed. Morally it would probably mean to rename facts using that
symbolic identifier instead of ASCII.


Moreover, HOL/Nonstandard_Analysis/NSComplex.thy provides another odd
const "iii" for "star_of \<i>". Maybe this could be improved after the
release as well.  Much of the "star" notation looks very old and could
benefit from present-day notational facilities.


	Makarius





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