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

  theory Thy1
  imports "Subdir/Thy2"

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.

Greetings,
Stefan

--
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 MHonArc.