Florian Haftmann wrote:
> The overloaded infix syntax "^" for different power operations (natural
> power in monoids, function power, relation power) turns more and more
> unsatisfactory for a couple of reasons, e.g.:
>
> * The abuse of the type class mechanism to achieve the "^" syntax for
> funp
On Tue, 2 Sep 2008, David Aspinall wrote:
> > You can achieve the above "name space effect" of symbols already via
> > something like \,
>
> Aha -- we can easily do this in PG then instead of \.
>
> > which is presently unused because LaTeX output is a bit strange (as for
> > \).
>
> The idea
On Tue, 2 Sep 2008, David Aspinall wrote:
> \
>
> \
>
> This is already supported in the X-Symbol replacement in the CVS version of
> Proof General, by the way, although Isabelle's lexer currently only allows
> syntax like \ and \.
The \ notation is more fundamental, below lexing even. It
> You can achieve the above "name space effect" of symbols already via
> something like \,
Aha -- we can easily do this in PG then instead of \.
> which is presently unused because LaTeX
> output is a bit strange (as for \).
The idea is to make the output the same as \, of course (with the
The overloaded infix syntax "^" for different power operations (natural
power in monoids, function power, relation power) turns more and more
unsatisfactory for a couple of reasons, e.g.:
* The abuse of the type class mechanism to achieve the "^" syntax for
funpow and relpow hinders the enforcemen
> There have been some thoughts to provide a mechanism of overloaded
> abbreviations or something similar to eliminate that problem
Yes --- I think the simplest thing is to simulate overloading by
extending Isabelle symbols with symbol variants, which automatically
have the same appearance but
Quoting Florian Haftmann :
> * funpow is defined as a separate primrec in theory Nat, without special
> syntax.
> * The remainder of theory Relation_Power is moved to Library, with a new
> infix syntax (e.g. "^^") for relpow.
> * The simple pow "^" then is just a primrec in class comm_monoid_mult
