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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
