Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Auto-suggest-theorem not working?


view this post on Zulip Email Gateway (Aug 22 2022 at 14:13):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
In Isabelle2016-1-RC1 I no longer observe the very useful behavior
that when I am typing a "using" clause when I enter the prefix
of the name of a theorem a tooltip pops up with theorems that
match the portion of the name I had entered.

I was enjoying this feature very much in Isabelle2016. It seemed
somehow also to sort the theorems by some kind of relevance criteria,
though that might have been my imagination. Is this feature
broken/deleted in the release candidate, or do I just not know how
to turn it on?

- Gene Stark

view this post on Zulip Email Gateway (Aug 22 2022 at 14:13):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Never mind. It seemed not to be working for awhile, but now it is
working again. I have no idea about that.


Last updated: Apr 25 2024 at 20:15 UTC