[isabelle-dev] Relation_Power.thy

[David Aspinall]

> 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).

  - D.

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.