Re: [isabelle] Concrete Syntax in locale
The "official" syntax declaration for a single subscript in locales is
with \<index> and your declaration would be:
locale X =
fixes e :: "'a => 'a" ("e\<^index>")
The corresponding syntax is "e\<^bsub> f a b <^esub>", for example.
I would advise against a translation from "e\<^bsub> f a b <^esub>" to
"e\<^sub>x". This looks very fragile.
Apart from that, I'm unfortunately unable to tell you what the correct
translation would be. Makarius is, but he unlikely reading e-mail for
the next two weeks.
This archive was generated by a fusion of
Pipermail (Mailman edition) and