Re: [isabelle] how do I find out which directory my theory file is in?
On Fri, 7 Jul 2006, Michael Norrish wrote:
> > To make a long story short, just do something like ``use
> > "myfile.ML"'' to refer to auxiliary files within the same directory
> > as the current thy source.
> Yes. In this case, I'm loading C files with a custom piece of code,
> so I need to make my code as smart as "use".
So maybe ThyLoad.check_file is what you want, e.g.:
ThyLoad.check_file NONE (Path.basic "Primes.thy");
(This example finds a file through the "$ISABELLE_HOME/src/HOL/Library"
This archive was generated by a fusion of
Pipermail (Mailman edition) and