Email Gateway (Aug 22 2022 at 18:55): Email Gateway (Aug 22 2022 at 18:55):From: jackx <xf930813@foxmail.com>
Why do I open hol, it shows: can not update the finished theory "HOL.HOL" error?
r.jpg
Email Gateway (Aug 22 2022 at 18:56):From: Makarius <makarius@sketis.net>
See this quote from the Isabelle/jEdit manual, section 3.5 (e.g. via the
Documentation panel in the Prover IDE):
Note that the link target may be a file that is itself not subject to
formal
document processing of the editor session and thus prevents further
exploration: the chain of hyperlinks may end in some source file of the
underlying logic image, or within the ML bootstrap sources of
Isabelle/Pure.
That manual has many more tips on how to use the Prover IDE front-end
effectively.
Makarius
Email Gateway (Aug 22 2022 at 18:56):From: Lawrence Paulson <lp15@cam.ac.uk>
Put another way: were you intending to actually update the theory HOL, or merely take a look at it? You can look the theories that make up Isabelle/HOL, but (especially as a new user) you shouldn’t be trying to change them.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC