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.
If you are using Isabelle 2017, and have downloaded your AFP directory to
/home/myself/afp , you should run the following command
[1] to make the AFP session ROOTS available to Isabelle:
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2017/ROOTS
You can now refer to article ABC from the AFP in some theory of
yours 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.
[1]: Tested for Linux and Mac installations ‐ it should be the same under cygwin on Windows.
|