Re: [isabelle] Adding search paths and importing theories



On Mon, 17 Mar 2008, Nicole Rauch wrote:

> 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.

> 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

> 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.

This is correct.  The load path cannot be changed during loading.  
Luckily there is no need to change it at all, just specify the import as 
follows:

  theory Test
  imports Main "~~/src/HOL/Word/Num_Lemmas"
  begin
 
  ...


	Makarius





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