Commit d11e5207 authored by kleing's avatar kleing
Browse files

instructions on how to refer to AFP entries

parent 18461115f798
<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<table width="100%">
<td width="20%" align="center" valign="top">
<!-- navigation -->
<!--#include file="nav.html"-->
<td width="80%" valign="top">
<!-- content -->
<div align="center">
<h1><font class="first">R</font>eferring to
<font class="first">AFP</font>
<font class="first">E</font>ntries</h1>
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.
<p>Let <code>PATH</code> be the absolute path where you have put the unpacked
AFP directory that you downloaded. Add <code>PATH</code> on a separate line to
the file <code>~/.isabelle/IsabelleXYZ/etc/components</code>, where XYZ is the
Isablle release you are working with, for example XYZ=2012. (In case you are
working with the development version of Isabelle, the file is simply
~/.isabelle/etc/components). You may need to create this file.</p>
You can now refer to article <code>ABC</code> from the AFP in some theory of
yours via</p>
<p><code>imports "$AFP/ABC"</code></p>
<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
Example: you are using Isabelle2012, and have downloaded your afp directory to
<code>~/isabelle/afp</code>. You would add the line
<code>~/isabelle/afp</code> to the file <code>~/.isabelle/components</code>.
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