Gergely Buday (Sep 13 2023 at 12:37): Gergely Buday (Sep 13 2023 at 12:37):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?
Fabian Huch (Sep 13 2023 at 15:02):You can start jedit with base logic Pure (isabelle jedit -l Pure) instead of the default HOL.
Wolfgang Jeltsch (Sep 13 2023 at 17:04):Which would have the exact opposite effect of what we discussed as a solution in the thread “Continuous ML Cleanup”. :wink:
Mathias Fleury (Sep 13 2023 at 17:06):The alternative it to generate and view the HTML , where click works
Wolfgang Jeltsch (Sep 13 2023 at 17:08):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: May 01 2024 at 20:18 UTC