Re: [isabelle] RC1: Immediate completion on \-symbols

I'm used to using jedit's built-in abbreviation facility. Could you briefly explain what is different about this new one?


> On 22 Jan 2016, at 18:01, Makarius <makarius at> wrote:
> you can use the 
> new etc/abbrevs facility to define your own special abbreviations.

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