Marvin Brieger (Sep 08 2023 at 10:25): Marvin Brieger (Sep 08 2023 at 10:25):Hey there,
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?
Best,
Marvin
Lukas Stevens (Sep 08 2023 at 12:22):You can launch Isabelle with isabelle jedit -l Pure
Lukas Stevens (Sep 08 2023 at 12:23):This uses 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: Apr 28 2024 at 12:28 UTC