[isabelle-dev] [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main
lp15 at cam.ac.uk
Mon Feb 27 18:22:47 CET 2017
Is it time to implement this change, regarding the imaginary constant ii?
Note: I have no suggestions for improving the star notation of non-standard analysis, mentioned in the last paragraph.
> On 19 Nov 2016, at 19:48, Makarius <makarius at sketis.net> wrote:
> 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 <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 <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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev