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

Hi John,

> 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".

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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.