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.
Linux/Mac
Assuming you have downloaded and unzipped the afp to /home/myself/afp , run
isabelle components -u /home/myself/afp/thys
Windows
If the AFP is in C:\afp , run the following command in a Cygwin terminal:
isabelle components -u /cygdrive/c/afp/thys
Use
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.
|