Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems loading example theories into PG

Email Gateway (Aug 18 2022 at 14:19):

From: munddr@googlemail.com
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

Email Gateway (Aug 18 2022 at 14:19):

From: Makarius <makarius@sketis.net>
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

Last updated: Apr 23 2024 at 16:19 UTC