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

2017-03-03 Thread Lawrence Paulson 
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 NSA: the prefixes 
hr and NS. 

A lot of work needs to be done in order to bring this development up-to-date. 
I’m glad to see that the star operator is now fully integrated into the 
axiomatic type class system, but quite a lot of material made redundant by that 
step is still present.

Larry

> On 3 Mar 2017, at 09:28, Makarius  wrote:
> 
> 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
> 
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2017-03-03 Thread Makarius 
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


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2017-02-27 Thread Lawrence Paulson 
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 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 \, 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 \);
>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 \ 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 \". 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