Isabelle proof source files are called Theories. Sessions are Isabelle's concept of grouping theories into coherent packages (cf. "component"/"module", "(software-)library").

For basic information on imports see Theories and Imports in the overview. See also system.pdf ch. 2 Isabelle sessions and build management.

Standard libraries (those .thy files bundled with Isabelle releases in the src/ directory) can be imported using a package-like syntax:

Imports containing special characters, like dashes -, must be surrounded by double quotes.

The session HOL is active per default (see Mechanics below), such that the theory src/HOL/Main.thy can be imported using just Main.

Files in the same directory as the importing file can be accessed by just the theory name. So for instance a session called OtherExample.thy can be imported as OtherExample, or (in case of name conflicts) through its qualified name in the virtual package Draft as Draft.OtherExample. Files in other directories can be imported using their relative paths, for example "Dir1/Thy1" (the quotes are required, as the slash / is a special character).

See also Creating Sessions below for a way to make theories available for import in other sessions.

The Archive of Formal Proofs is a growing collection of sessions. It is not included with Isabelle distributions per default, so using the libraries requires prior setup:

Download the version of the AFP that corresponds to the version of Isabelle from the downloads section. Note that downloading the wrong version may result in errors and warnings in the underlying proofs.

Follow the instructions at Referring to AFP Entries (download and unpack AFP release, run isabelle components -u path/to/afp/thys). Note that for Windows, the command has to be entered in the cygwin terminal (<isa install dir>/Cygwin-Terminal.bat), and the path to the AFP installation has to be adapted to fit the cygwin scheme /cygdrive/<drive letter>/path/to/afp/thys. The command isabelle components -u ... is equivalent to adding the path manually to $ISABELLE_HOME_USER/ROOTS.

After setup, AFP entries can be accessed like standard libraries.

When importing sessions, all stated results and proofs will be checked in the same way that code is executed live in the Isabelle/jEdit. This may take some time depending on the size of the sessions. The import progress can be tracked in the Theories panel in Isabelle/jEdit, docked on the right by default, otherwise accessible via Plugins > Isabelle > Theories panel (see also jedit.pdf ch. 3.1.2 Theories). Additionally, all loaded sessions will be displayed there.

Members of the sessions HOL (like Main) are exceptions to this as they are part of the pre-compiled session image HOL which is loaded per default at startup (the same applies to the session Pure). The loaded session image can be changed in the Theories panel in Isabelle/jEdit (changes will take effect after a restart of Isabelle/jEdit). If a session image is not yet compiled or out of date (newer sources available), it will be rebuilt on startup. Session images that are included with the distribution are stored in $ISABELLE_HOME/heaps/ and user compiled ones in ~/.isabelle/Isabelle<version>/heaps/.

Note that while changing the session image may result in faster startup times, it prevents the semantic highlighting in Isabelle/jEdit to work properly for any theories of the loaded session (indicated by the warning Cannot update finished theory ...). To work around this, change the session image to one that does not include the relevant theories and restart Isabelle/jEdit. Normally, the default HOL is sufficient; for inspecting parts of HOL, one may use Pure. Alternatively, import the theory in question as a file, by specifying its path either absolute or relative to the current file (it may be necessary to restart the IDE or purge loaded theories).

The session HOL-Proofs is special in that the image includes the full proof terms of the entire HOL-Library.

In order for Isabelle to recognize a session, it has to be defined in a ROOT file.

(* ROOT (example) *)
session Example_Session = HOL +
  sessions
    "HOL-Library"
  theories
    Example_Theory

Any sessions from which theories are imported must be listed here. While it is not necessary to extend some parent session (here HOL), it is highly recommended. If Example_Theory imports some Other_Theory from the same directory, it will automatically be included.

Isabelle/jEdit provides semantic highlighting and checking for ROOT files.
See system.pdf ch. 2.1 Session ROOT specifications for ROOT file structure and syntax.

The built-in command isabelle mkroot (see system.pdf ch. 3.2) generates a stub ROOT file.

In order to use a session in Isabelle, its ROOT has to be referred to in a ROOTS file (points to directories with ROOT files or further ROOTS).

(* ROOTS (example) *)
some/path
/some/absolute/path

There are two main ROOTS for each Isabelle installation: one in the installation directory ($ISABELLE_HOME) that should not be edited, and one in ~/.isabelle/Isabelle<version>/ ($ISABELLE_HOME_USER).

In addition, the Isabelle CLI provides a shortcut for adding paths to the main user-ROOTS: isabelle components -u path/to/thys.

See also system.pdf ch 2.3.

It is recommended to include a ROOT file in the session's base directory. See for instance the AFP Example-Submission (contains rules and recommendations for AFP Submissions).

Since only a single compiled session image can be loaded at startup, working on theories that depend on multiple large sessions, such as HOL-Analysis and Graph_Theory, can be tedious, Isabelle/jEdit still needs to check at least one session at each startup. To avoid this, developers can create a dummy session containing all dependencies (but no actual code).

A simple setup for this looks as follows (with dev-session included in a ROOTS file):

dev-session/
  ROOT
  DEV.thy

File contents:

(* ROOT *)
session "DEV_Something" = "<session1>" +
  sessions "<session2>" "<session3>"
  theories "DEV"

(* DEV.thy *)
theory DEV
  imports "<session1>.<theory1>" "<session2>.<theory2>" "<session3>.<theory3>"
begin
end

It is advisable to be generous at importing theories in such a session, as each addition or change will require rebuilding the session. Similarly, when checking such a session into VCS, it should be consistent across branches.

An important choice is which session to choose as the "parent" session (<session1> in this example), as this session can be compiled independently of the DEV session. This should be the "largest" session, the one which takes the longest to compile, and, ideally already is compiled. For most purposes, this can be HOL-Library (because of its wide range) or a session that includes it.