[isabelle-dev] Relation_Power.thy

[Makarius]

On Tue, 2 Sep 2008, David Aspinall wrote:

>   \<caret:funpow>
> 
>   \<caret:relpow>
> 
> 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 \<caret1> and \<caret2>.

The \<symbol> notation is more fundamental, below lexing even.  It is 
actually fashioned after Java's \uDDDD for UTF-16 chars, but we do not 
depend on unicode encoding variants of course.

You can achieve the above "name space effect" of symbols already via 
something like \<caret_funpow>, which is presently unused because LaTeX 
output is a bit strange (as for \<caret1>).  This means \<foo_bar> and 
\<foo42> are both unlikely to be used already for something else.

There is also a more compositional way to produce symbol variants: 
\<^control>\<symbol>.  Here nothing needs to be changed in Isabelle, only 
the UI needs to provide sane input methods and proper display (without the 
flashing of x-symbol for \<^sub> for example).


	Makarius