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,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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