[isabelle] Tuning opportunity for auto-completion in Isabelle/Jedit


I noticed that when listing completions (in Isabelle/Jedit) for

  thm ex     or     thm ext

(with the cursor after the x and t respectively), the fact "ext"
is not listed. I found this rather surprising.

This happens with both Isabelle 2014 and 2015 RC0, in a trivial
theory file that just imports Main.



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