[isabelle-dev] Relation_Power.thy

[David Aspinall]

> 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 different underlying meaning, e.g.

   \<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>.  If you're worried which 
symbol you're looking at, you wave your mouse at it.  See 
etc/isar/TokensAcid.thy for an example.

  - David

PS I also have a patch to implement this in X-Symbol but would rather 
let X-Symbol die.

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