Re: [isabelle] Problems loading example theories into PG



On Tue, 17 Nov 2009, munddr at googlemail.com wrote:

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

This looks like you are trying to load Isabelle/FOL examples into
Isabelle/HOL.  To build a proper FOL image, just run

  Isabelle2009/build FOL

on the command line.

Afterwards Proof General will offer the new logic image in one of the menus.


	Makarius





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