[isabelle-dev] Mirabelle and load path

[Makarius]

On Fri, 4 Mar 2011, Alexander Krauss wrote:

> So I am wondering if the system could provide a variant of use_thy(s), 
> which takes an explicit master path and basically interprets the given 
> theory as if it would reside in that path. Probably, similar 
> functionality is already available for PG interaction. Of course any 
> other solution would be fine as well...

It should be sufficient to include the path in the use_thy invocation:

   use_thy "/tmp/A.thy";

Alternatively there is

   Thy_Info.use_thys_wrt: Path.T -> string list -> unit


 	Makarius