Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] novice problem about loading theorey file

Email Gateway (Aug 17 2022 at 13:28):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
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
Isabelle2005:

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

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

Cheers,
Gerwin

Last updated: Nov 21 2024 at 12:39 UTC