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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and