Re: [isabelle] using files
Jeremy Dawson wrote:
I find that sometimes (unpredictably) "use"ing a file uses the "wrong"
file, for example in the src/HOL directory,
What exactly does ThyInfo.use do to decide what file to use?
The file name supplied as an argument to the use command is interpreted
relative to the location of the theory last loaded. For example, if the
theory Thy1 imports a theory Thy2 located in subdirectory Subdir via
then all use commands in *.ML files loaded by theory Thy2 refer to the
files in directory Subdir, and not in the directory containing Thy1.
If use seems to act strangely, then this is probably caused by the
the current context (which you can inspect via "the_context()") being
set to the "wrong" theory.
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3 Room: 01.11.059
85748 Garching, GERMANY http://www.in.tum.de/~berghofe
This archive was generated by a fusion of
Pipermail (Mailman edition) and