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: Feb 28 2025 at 08:24 UTC