[isabelle-dev] Extracting dependencies from theory headers

Makarius makarius at sketis.net
Thu Dec 30 21:21:11 CET 2010

On Thu, 30 Dec 2010, John Matthews wrote:

> Another question: If the user asks Isabelle to process theory A, and 
> theory A has statement
> imports "dir1/B"
> and theory B has statement
> imports "dir2/C"
> then will Isabelle look for theory C in dir1 or dir1/dir2 ?
> In other words, does master_dir change to the enclosing directory of the 
> theory being imported?

Yes, the master directory changes accordingly.  This is what I meant with 
the sentence below:

> On Dec 30, 2010, at 5:17 AM, Makarius wrote:
>> the master directory, which is the location of the enclosing theory 
>> file when traversing the import graph.

Here is also the ML version of it: 

The idea is that resources are references relatively to each theory node, 
without any further complications getting in between.


More information about the isabelle-dev mailing list