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.

Clemens






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