Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Error: 'Cannot update finished theory'

view this post on Zulip Email Gateway (Aug 18 2022 at 14:21):

From: John Munroe <munddr@googlemail.com>
Hi,

I'm trying to load OrderedGroup.thy into PG, but I keep getting the
error saying:

*** Theory loader: cannot update finished theory "OrderedGroup"
*** At command "theory".

I've already built HOL and HOL-Algebra and have tried both HOL and
HOL-Algebra from the Isabelle|Logic menu.

Any help will be appreciated.

Thanks
John

view this post on Zulip Email Gateway (Aug 18 2022 at 14:21):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,

OrderedGroup.thy is part of the HOL image already. To use a refined
version of it, you must load an image which does not already contain
OrderedGroup.thy. In your case the HOL-Base image (since Isabelle2009)
is suitable: switch to directory "src/HOL" and execute "isabelle make
HOL-Base". After that PG will offer you HOL-Base in menu
Isabelle/logics. Select this and use OrderedGroup.thy interactively.

To understand dependencies among theories, the diagnostic Isar command
"thy_deps" may prove helpful.

Hope this helps,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC