On Tue, 2012-11-20 at 15:24 +0100, Makarius wrote: > I have many more things on my list to improve the completion mechanism, > before such a detail would be considered again.
A huge step forward, in my humble opinion, would be context-sensitive completion. For instance, I would ideally like the IDE to figure out whether I am typing "le" to obtain "lemma" or "≤". If this works well, one could then also consider completion for methods, theorem names, logical constants, and whatnot. Anyway, just dreaming. Best regards, Tjark _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
