Re: [isabelle] Concrete Syntax in locale



On Fri, 24 Mar 2006, Peter Lammich wrote:

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

Note that \<^sub> cannot really be used like this, because it operates on 
a single symbol only.  The argument filled in for 'a can be anything, not 
just variables of > 1 letters, but arbitrarily complex terms.


> Now I want also inputs like "e\<^bsub> f a b <^esub>" to be mapped to 
> this symbol.

Better use this form exclusively.  Proof General provides a key sequence 
that makes it as easy to enter as \<^sub> (see describe-mode).


	Makarius





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