[isabelle-dev] Relation_Power.thy

David Aspinall da at inf.ed.ac.uk
Tue Sep 2 16:57:02 CEST 2008

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



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.

More information about the isabelle-dev mailing list