Re: [isabelle] novice problem about loading theorey file

On Thursday 24 November 2005 14:44, Chen Chunqing wrote:
> Can anyone teach me how to load an established theory file which is not
> in the same directory? Thanks in advance.

The way Larry wrote is the right one for using the real numbers etc.

In case you really need something in the future that is not in an image, but 
can be found in a different directory, you can write the following in 

theory X
imports "../some/path/Y"
imports "~~/src/HOL/some/example/Z"

The first just is a path relative to the location of X. In the second path, 
"~~" stands for $ISABELLE_HOME.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.