Re: [isabelle] change proposal: eliminating overloading for factorials

On Mon, 2 Mar 2015, Manuel Eberl wrote:

There is also ALL and EX as already existing replacement ASCII syntax for ! and ?. I usually type ALL when I want to enter â anyway; it doesn't seem to work with EX though.

The Isabelle/jEdit manual has a long explanation on completion. The above case falls under "Input events" for "syntax keywords" (because some alphabetic text is to be replaced). It says:

  \item Completion of syntax keywords requires at least 3 relevant
  characters in the text.

Explicit completion always works, regardless of the input length.

Anyway, I consider the replacements of ALL, EX etc. as *very* nostalgic.


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