[isabelle-dev] Relation_Power.thy

[Makarius]

On Tue, 2 Sep 2008, David Aspinall wrote:

> > You can achieve the above "name space effect" of symbols already via
> > something like \<caret_funpow>,
> 
> Aha -- we can easily do this in PG then instead of \<caret1>.
> 
> > which is presently unused because LaTeX output is a bit strange (as for
> > \<caret1>). 
> 
> The idea is to make the output the same as \<caret>, of course (with the
> disadvantage that you can't wave your mouse over a piece of paper).

You can, if it is electronic paper like PDF or even DVI (using recent 
link-enabled xdvi, for example).


	Makarius