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

As I understand it, the star notation is the standard way of denoting the injection of an entity from, say, the standard reals to the non-standard reals. It is normally written as a prefix operator. Maybe we could do something using our ⋆ character. But we have two other naming conventions in

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

On 27/02/17 18:22, Lawrence Paulson wrote: > > Note: I have no suggestions for improving the star notation of > non-standard analysis, mentioned in the last paragraph. Can you point to some literature or papers that use the notation in a canonical form? Makarius

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

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 wrote: > > Here is also