Referring to AFP Entries


Once you have downloaded the AFP, you can include its articles and theories in your own developments. If you would like to make your work available to others without having to include the AFP articles you depend on, here is how to do it.

From Isabelle2021-1 on, the recommended method for making the whole AFP available to Isabelle is the isabelle components -u command.


Assuming you have downloaded and unzipped the afp to /home/myself/afp, run

    isabelle components -u /home/myself/afp/thys


If the AFP is in C:\afp, run the following command in a Cygwin terminal:

  isabelle components -u /cygdrive/c/afp/thys


You can now refer to article ABC from the AFP in another theory via

    imports "ABC.Some_ABC_Theory"

This allows you to distribute your material separately from any AFP theories. Users of your distribution also need to install the AFP in the above manner.