Commit 69cf96dd authored by gerwin.klein@nicta.com.au's avatar gerwin.klein@nicta.com.au
Browse files

submission system only allows "../entry/thy" method

parent ff1f8e03c75b
......@@ -58,13 +58,18 @@ theories. Users of your distribution also need to install the AFP in the above
manner.</p>
<p>
Note that referring to <strong>another AFP entry from inside an AFP
entry</strong> is much easier:
entry</strong> is different and much easier:
<pre class="code">
imports "../ABC/Some_ABC_Theory"
</pre>
This is the preferred method for working inside the AFP,
because it interacts correctly with multiple AFP installations side by side.
For working inside the AFP, this is the mandated option.
It interacts correctly with multiple AFP installations side by side.
</p>
<p>You can also use this method in your own work outside the AFP, you only
need to place the AFP entries you refer to next to your development in the
correct location in the directory hierarchy.</p>
<p>&nbsp;</p>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment