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

[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 <makarius at sketis.net> 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
> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170303/f5c6a140/attachment-0002.html>