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