Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] imports?

view this post on Zulip Email Gateway (Aug 18 2022 at 13:36):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
I'm deep into not understanding something(s). Start with this:

In standard Isabelle 2009 HOL-Nominal

theory test
imports FuncSet
begin

works fine. Somehow (?) Isabelle looked for "FuncSet" in
Isabelle/HOL/HOL-Algebra. However

theory test
imports FuncSet Lattice
begin

fails with

*** Could not find theory file "Lattice.thy" in ".", "/home/rpollack/work/CISA/graphicalLocic", "$ISABELLE_HOME/src/HOL/Library"

even though "Lattice" is in the same directory as FuncSet (which, BTW,
is not any of the directories listed).

BTW, "imports FuncSet Lattice" comes from the header of
Isabelle/HOL/HOL-Algebra/Group, which I was trying to load.

What is going on, and how do I fix it?

Best,
Randy

view this post on Zulip Email Gateway (Aug 18 2022 at 13:37):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Randy,

this is a misunderstanding: theory FuncSet resides in HOL/Library, which
is part of the theory search part; to get access to Algebra/Lattice,
the easiest way is to use a full path:

theory test
imports FuncSet "~~/src/HOL/Algebra/Lattice"
begin

where Isabelle internally expands ~~ to the root directory of the
distribution.

Hope this helps
Florian
signature.asc

Last updated: May 03 2024 at 08:18 UTC