Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Trouble loading theories on windows (Isabelle2...


view this post on Zulip Email Gateway (Aug 19 2022 at 12:16):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,

This is a continuation of this thread: "[isabelle] Trouble loading
theories on windows":

http://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-August/msg00050.html

It's not specific to Isabelle2013-1, but I go ahead and associate it
with Isabelle2013-1-RC3.

The suggestions are to save and reload the theory, but that doesn't work
for me when I use this:

theory c
imports Complex_Main "~~/src/HOL/Library/Fset"

The file Fset.thy gets loaded into jEdit, but I still get this error:

Bad theory (file "E:\E_2\binp\Isabelle2013-1-RC3\src\HOL\Library\Fset.thy")

So, I use a relative path:

theory c
imports Complex_Main

"../../../../../../E_2/binp/Isabelle2013-1-RC3/src/HOL/Library/Fset"

The file Fset.thy gets loaded, I get no errors, and I don't have to do
anything special.

Regards,
GB


Last updated: Apr 25 2024 at 16:19 UTC