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

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:

Here the notation was changed to the current \<i>, without changing the
const name:

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.


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