This instance will be upgraded to Heptapod 0.23.2 on 2021-08-05 at 11:00 UTC+2 (a few minutes of down time)

using.tpl 1.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
{% extends "base.tpl" %}

{% block headline %}
<font class="first">R</font>eferring to
<font class="first">A</font>FP
<font class="first">E</font>ntries
{% endblock %}

{% block content %}
<table width="80%" class="descr">
  <tbody>
    <tr><td>

<p>
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
<i>without</i> having to include the AFP articles you depend on, here is how to do it.
</p>
<p>
Gerwin Klein's avatar
Gerwin Klein committed
20
If you are using Isabelle2020, and have downloaded your AFP directory to
21 22
<code>/home/myself/afp</code>, you should run the following command
<a href="#1">[1]</a> to make the AFP session ROOTS available to Isabelle:</p>
23 24
<p>
<pre class="code">
Gerwin Klein's avatar
Gerwin Klein committed
25
    echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2020/ROOTS
26 27 28 29 30 31 32
</pre>

<p>
You can now refer to article <code>ABC</code> from the AFP in some theory of
yours via</p>

<pre class="code">
33
    imports "ABC.Some_ABC_Theory"
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
</pre>

<p>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.</p>

<p>&nbsp;</p>

<p>
<a name="1">[1]:</a> Tested for Linux and Mac installations &dash; it should be the same under cygwin on Windows.
</p>
<p>
    </td></tr>
  </tbody>
</table>
{% endblock %}