Email Gateway (Aug 18 2022 at 14:19): 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: Nov 21 2024 at 12:39 UTC