[isabelle] Concrete Syntax in locale
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.
"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