Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] why it wrong?


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 08:18 UTC