Gergely Buday (Oct 20 2023 at 12:49): Gergely Buday (Oct 20 2023 at 12:49):When I want to use a theorem name, like myfun_def, I start to type
have " statement " unfolding myfun_def
Sometimes, after typing a few letters from myfun_def Isabelle/jEdit gives me a list of possible expansions, but sometimes not.
What does this depend on?
Last updated: Nov 07 2025 at 16:23 UTC