diff --git a/metadata/templates/using.tpl b/metadata/templates/using.tpl --- a/metadata/templates/using.tpl +++ b/metadata/templates/using.tpl @@ -1,58 +1,58 @@ {% extends "base.tpl" %} {% block headline %} Referring to AFP Entries {% endblock %} {% block content %}
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 on, the recommended method for making the whole AFP available to Isabelle
+From Isabelle2021-1 on, the recommended method for making the whole AFP available to Isabelle
is the Linux/Mac
Assuming you have downloaded and unzipped the afp to isabelle components -u /home/myself/afp/thys Windows
If the AFP is in isabelle components -u /cygdrive/c/afp/thys Use
You can now refer to article 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.
|