This section focuses on the Archive of Formal Proofs. For help with Isabelle, see the Isabelle Documentation. More resources are listed in the Isabelle Quick Access Links.
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-1 on, the recommended method for making the whole AFP available to Isabelle is the isabelle components -u command.
Assuming you have downloaded and unzipped the afp to /home/myself/afp, run:
isabelle components -u /home/myself/afp/thys
If the AFP is in C:\afp, run the following command in a Cygwin terminal:
isabelle components -u /cygdrive/c/afp/thys
You can now refer to article ABC from the AFP in another theory 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.
The following gives an example of the preferred way for citing entries in the AFP:
M. Jaskelioff and S. Merz, Proving the Correctness of Disk Paxos. Archive of Formal Proofs, June 2005, https://isa-afp.org/entries/DiskPaxos.html, Formal proof development.
The bibtex entry for this would be:
@article{Jaskelioff-Merz-AFP05,
author = {Mauro Jaskelioff and Stephan Merz},
title = {Proving the Correctness of Disk Paxos},
journal = {Archive of Formal Proofs},
month = Jun,
year = 2005,
note = {\url{https://isa-afp.org/entries/DiskPaxos.html}, Formal proof development},
ISSN = {2150-914x}
}
isabelle-users@cl.cam.ac.uk provides a forum for Isabelle users to discuss problems, exchange information, and make announcements. Users of official Isabelle releases should subscribe or see the archive.
isabelle-dev@in.tum.de covers the Isabelle development process, including intermediate repository versions, and administrative issues concerning the website or testing infrastructure. Early adopters of development snapshots or repository versions should subscribe or see the archive (also available at mail-archive.com).