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: Dec 21 2024 at 12:33 UTC