Please send your submission
via this web page.
The submission must follow the following Isabelle style rules.
For additional guidelines on Isabelle proofs, also see the this guide (feel free to follow all of these; only the below are mandatory).
Technical details about the submission process and the format of the submission are explained on the submission site.
- No use of the commands
- Instantiations must not use Isabelle-generated names such as
xa — use Isar, the
rename_tac to avoid such names.
- No use of the command
- If your theories contain calls to
nunchaku those calls must
expect parameter. Alternatively the
expect parameter must be set globally via, e.g.
apply scripts should be indented by subgoal as in
the Isabelle distribution. If an
apply command is
applied to a state with
n+1 subgoals, it must be
n spaces relative to the first
apply in the sequence.
- Only named lemmas should carry attributes such as
- We prefer structured Isar proofs over apply style, but do not
- If there are proof steps that take significant time, i.e. longer
than roughly 1 min, please add a short comment to that step, so
maintainers will know what to expect.
It is possible and encouraged to build on other archive entries
in your submission. There is a standardised way to
refer to other AFP entries in your
Your submission will be refereed and you will receive notification
as soon as possible. If accepted, you must agree to maintain your
archive entry or nominate someone else to maintain it. The Isabelle
development team will assist with maintenance, but it does not have the
resources to fully maintain the complete archive.
If you have questions regarding your submission, please email email@example.com.
If you need help with Isabelle, please use the
mailing list. It is always a good idea to subscribe.