Re: [isabelle] jEdit: cursor movement and goal display



On Wed, 23 May 2012, Christian Sternagel wrote:

The word "and" should not expand to the symbol "∧".

Let's say it does not expand. I am unsure if it should or not. The behaviour stems from the overlap of symbol name with outer keyword.

Anyway, completion should become more context sensitive at some point. Within a term, "and" does not have any special meaning.


	Makarius


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