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.
Larry Paulson > On 19 Nov 2016, at 19:48, Makarius <makar...@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. >
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
