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 <makar...@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 > >
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
