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