in theories I wrote my self and in theories I downloaded from the AFP, I can usually navigate once the are processed by ctrl+clicking onto symbols in order to go to the place where the symbol is defined.
In finished theories from Main this does not work out of the box as the files are not processed since they are finished. However, this is very inconvenient when one would like to lookup the definition of a symbol in such a finished theory.
Is there a way to get the finished theories processed or any other workaround?
You can launch Isabelle with
isabelle jedit -l Pure
Pure as the base logic instead of
HOL. The disadvantage is that you need a lot more RAM and it takes longer, since you are not using the prebuilt HOL image any more.
Last updated: Dec 07 2023 at 20:16 UTC