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