[isabelle] Concrete Syntax in locale



Hi,

I have some 

locale X =
  fixes e :: "'a => 'a" ("e\<^sub>_")

so that for instance e\<^sub>x gets mapped to this symbol.
Now I want also inputs like "e\<^bsub> f a b <^esub>" to be mapped to this
symbol. How to do that on syntactical level, without fixing and defining a
second symbol in the locale ?

thanks for any help in advance.

--peter

-- 
"Feel free" mit GMX FreeMail!
Monat für Monat 10 FreeSMS inklusive! http://www.gmx.net





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.