I get the
Cannot update finished theory "HOL.Groups_Big"
error message on opening a theory file in the HOL distribution.
Also, Ctrl-click does not work on identifiers here, which might be related. Is there a workaround for this?
You can start jedit with base logic Pure (
isabelle jedit -l Pure) instead of the default HOL.
Which would have the exact opposite effect of what we discussed as a solution in the thread “Continuous ML Cleanup”. :wink:
The alternative it to generate and view the HTML , where click works
In the case of the standard library, you don’t even need to generate it yourself, as it is already online: https://isabelle.in.tum.de/library/.
Last updated: Dec 07 2023 at 08:19 UTC