[isabelle] Adding search paths and importing theories
today I ran into a problem of how to add a search path and to import a
theory that is to be found in the search path.
In order to make a search path available, I define a theory:
I then import that theory and simultaneously the theory that I
actually want to import:
imports Test1 Num_Lemmas
If I first load Test1 in Proof General and evaluate it, and afterwards
load Test2 in Proof General and evaluate it, everything works fine.
But if I start off with Test2, I get an error message that Num_Lemmas
cannot be found because Isabelle (being strict) obviously first tries
to locate all imports before evaluating them.
I've also tried to add the ML command to the very top of Test2 (before
the theory definition), and this works fine for Test2, but then I get
an error message when I try to import Test2 into some other theory
(the import mechanism expects the imported theories to start with
Is there any solution to this conflict? How can I make Isabelle first
load the first imported theory before loading the second one?
Thanks in advance for any help
This archive was generated by a fusion of
Pipermail (Mailman edition) and