[isabelle] Adding search paths and importing theories



Dear all,

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:

theory Test1
imports Main
begin

ML {*
add_path "$ISABELLE_HOME/src/HOL/Word";
*}

end

I then import that theory and simultaneously the theory that I actually want to import:


theory Test2
imports Test1 Num_Lemmas
begin

end

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 "theory").

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

Nicole






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.