The Archive of Formal Proofs is an online resource and therefore
more dynamic than a normal scientific journal. Existing entries
can and do evolve and can also be updated significantly by their
This conflicts with the purpose of archiving and preserving
entries as they have been submitted and with the purpose of
providing a clear and simple interface to readers.
The AFP deals with this by synchronizing such updates with
The entries released and visible on the main site are always
working with the most recent stable Isabelle version and do not
In the background, the archive maintainers evolve all entries to
be up to date with the current Isabelle development
version. Authors can contribute changes to this version which is
available as a bitbucket
mercurial repository or as tar.gz package on the download page.
When a new Isabelle version is released, the above mentioned
development version of AFP is frozen and turns into the main
version displayed on the front page. Older versions (including the
original submission) of all entries are archived and remain
If you are an author
The above means that if you are an author and would like to
provide a new, better version of your AFP entry, you can do so.
To achieve this, you should base your changes on the mercurial
of your AFP entry and test it against the current Isabelle development
If you would like to get write access to your entry in the
mercurial repository or if you need
assistance, please contact the editors.