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
isabelle components -u command.
Assuming you have downloaded and unzipped the afp to
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
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