[isabelle] Problems loading example theories into PG



Hi,

I'm trying to load some example theories into PG, but I keep getting errors.

With Nat.thy, I get an error saying 'Theory loader: cannot update finished theory "Nat"' at

theory Nat
imports FOL
begin

With Prolog.thy, I get:
'*** Could not find theory file "FOL.thy" in ".", "/usr/local/Isabelle2009/src/FOL/ex", "$ISABELLE_HOME/src/HOL/Library"*** Theory loader: the error(s) above occurred while examining theory "FOL"*** At command "theory".

Does anyone know what I'm missing here? Did I not set the path variables correctly?

Thanks
John




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