diff --git a/admin/publish b/admin/publish
--- a/admin/publish
+++ b/admin/publish
@@ -1,177 +1,177 @@
 #!/usr/bin/env bash
 #
 # Author: Gerwin Klein, NICTA
 #
 # publishes archive entry + main web pages on isa-afp
 #
 # This script expects Isabelle version >= 2008-10-05
 # (uses isabelle instead of isatool)
 
 ## settings
 
 source "$(dirname "$0")/common"
 
 AFP_VERSION=afp-$VERSION
 ISABELLE_VERSION="Isabelle${VERSION}"
 
 DEST=afpweb@isa-afp.org:
 FILES=frs.sourceforge.net:/home/frs/project/afp/afp-$ISABELLE_VERSION/
-SRC=ssh://hg@bitbucket.org/isa-afp/$AFP_VERSION
+SRC=ssh://hg@foss.heptapod.net/isa-afp/$AFP_VERSION
 
 if [ -n "$SF_LOGIN" ]; then
     LN=$SF_LOGIN
 else
     LN=$LOGNAME
 fi
 
 FILES=$LN@$FILES
 
 EXPORT_PRE=afp
 HG=hg
 DATE=`date '+%Y-%m-%d'`
 
 TAR=tar
 
 
 ## functions
 
 function usage()
 {
   echo
   echo "Usage: $PRG [options] [<entries>|-]"
   echo
   echo "  Checks out web site and archive entries and publishes them on the isa-afp.org web site"
   echo
   echo "Options:"
   echo "  -r                  use specified Isabelle version"
   echo "  -f                  do not ask before publishing"
   echo "  -t <isabelle> <tag> use specified path to isabelle tool script"
   echo
   echo "Examples:"
   echo "  $PRG -r 2009 Example-Submission"
   echo "  $PRG -t /usr/proj/Isabelle2009/bin/isabelle Isabelle2009 Example-Submission"
   echo
   echo "  $PRG Example-Submission"
   exit 1
 }
 
 ## argument checking
 
 [ "$#" -lt "1" -o "$1" = "-?" ] && usage
 
 INTERACTIVE="yes"
 
 while getopts "ft:r:" OPT
 do
     case "$OPT" in
       r)
         VERSION="$OPTARG"
         ;;
       f)
         INTERACTIVE="no"
         ;;
       t)
         ISABELLE_TOOL="$OPTARG"
         ISABELLE_VERSION="$1"
         shift
         ;;
     esac
 done
 shift $(($OPTIND - 1))
 
 set_isabelle_tool
 
 
 EXPORT=$EXPORT_PRE-$DATE
 
 ###
 
 WD="$(pwd)"
 cd "$DIR"
 ROOT="$(hg root)" || fail "could not obtain repo root"
 cd "$ROOT" || fail "could not cd to repo root"
 
 echo "Checking sync with $SRC"
-$HG outgoing $SRC && fail "Push changes to bitbucket first."
+$HG outgoing $SRC && fail "Push changes to Heptapod first."
 
 echo "Exporting from working copy $ROOT"
 HG_EXPORT=afp-export-$DATE
 rm -rf $HG_EXPORT
 $HG archive -I thys -I web -I etc -I tools $HG_EXPORT || fail "hg archive failed."
 cd $HG_EXPORT
 echo -n $DATE > web/release-date.txt
 mkdir $EXPORT
 mv thys etc tools $EXPORT/
 
 if [ "$1" != "-" ]; then
     echo "Cleaning up browser_info directory"
     BROWSER_INFO=`$ISABELLE_TOOL getenv -b ISABELLE_BROWSER_INFO` || fail "could not find browser info"
     [ -e "$BROWSER_INFO" ] && rm -rf $BROWSER_INFO
 
     HTML_THYS=web/browser_info/$ISABELLE_VERSION
     TARS=web/release
     mkdir -p $HTML_THYS
     ln -s $ISABELLE_VERSION web/browser_info/current
     ln -s ../front.css web/entries/front.css
     mkdir -p $TARS
 
     echo "Tarring [$EXPORT]"
     $TAR -cf $EXPORT.tar $EXPORT
     gzip --best -f $EXPORT.tar
     ln -s $EXPORT.tar.gz $TARS/afp-current.tar.gz
     mv $EXPORT.tar.gz $TARS/
 
     echo "Generating HTML for [$@]"
     $ISABELLE_TOOL afp_build -- -v -c $@  || fail "isabelle afp_build failed on [$@]"
 
     cd $EXPORT/thys
     for ENTRY in $@; do
         if [ -d $ENTRY ]; then
             echo "Tarring [$ENTRY]"
             $TAR -cf $EXPORT_PRE-$ENTRY-$DATE.tar $ENTRY
             gzip --best -f $EXPORT_PRE-$ENTRY-$DATE.tar
             mv $EXPORT_PRE-$ENTRY-$DATE.tar.gz ../../$TARS/
             ln -s $EXPORT_PRE-$ENTRY-$DATE.tar.gz ../../$TARS/$EXPORT_PRE-$ENTRY-current.tar.gz
             echo "Finished [$ENTRY]"
         fi
     done
     cd ../..
 
     echo "Copying generated HTML"
     for DIR in $BROWSER_INFO/*; do
         if [ -d $DIR ]; then
             cp -r $DIR $HTML_THYS
         fi
     done
 
     if [ "$INTERACTIVE" == "yes" ]; then
         echo "Web pages are prepared for publication under"
         echo "[`pwd`/web/]."
         echo "Please check content."
         read -n 1 -p "Type y if you want to publish. Any other key quits." RESPONSE
     else
         RESPONSE="y"
     fi
 else
     RESPONSE="y"
 fi
 
 if [ "$RESPONSE" == "y" ]; then
 #    if [ "$TARS" != "" ]; then
 #        echo
 #        echo "Pushing $EXPORT to [$FILES]"
 #        scp $TARS/$EXPORT.tar.gz $FILES
 #    fi
     echo
     echo "Publishing to [$DEST]"
     chmod -R g-w web
     chmod -R a+r web
     find web -type d | xargs chmod a+x
     chmod 755 web
     rsync -rplvz --links --rsh=ssh web/ $DEST && echo "Finished."
 else
     echo
     echo "Aborted."
     exit 1;
 fi
 
diff --git a/doc/editors/new-entry-checkin.md b/doc/editors/new-entry-checkin.md
--- a/doc/editors/new-entry-checkin.md
+++ b/doc/editors/new-entry-checkin.md
@@ -1,95 +1,100 @@
 New Submissions (editors only)
 ------------------------------
 
 **Mercurial Setup**
 
 As editor you have at least two working copies of the repository:
 current release branch and development version.
 
 -   Start by making a directory `~/afp` where the different branches
     will go.
 -   To set up the release version, in that directory do (fill in 20XX)
 
-        hg clone ssh://hg@bitbucket.org/isa-afp/afp-20XX release
+        hg clone ssh://hg@foss.heptapod.net/isa-afp/afp-20XX release
 
 -   for development
 
-        hg clone ssh://hg@bitbucket.org/isa-afp/afp-devel devel
+        hg clone ssh://hg@foss.heptapod.net/isa-afp/afp-devel devel
 
 You might need to set up ssh keys on Heptapod for this to work. This can
-be done under "Manage account/SSH Keys".
+be done under "[Settings/SSH Keys][keys]".
 
 New submissions, changes to the web site and to admin scripts go into
-afp/release. Gerwin merges these into the development version within a
-day or two.
+afp/release. About once a week, one of the editors should merge afp-release
+into afp-devel, ideally making sure after the merge that the entry works in
+the devel version, although that sometimes may be too much and be left for
+the authors to fix themselves.
 
 Maintenance and changes on existing submissions all occur in afp/devel
 and go properly public with the next Isabelle release (they are only
 available as (public) development tar.gz's)
 
+[keys]: https://foss.heptapod.net/profile/keys
+
 **New Submissions**
 
 Everything happens in the release branch `afp/release`.
 
 1.  unpack tar file and move new entry to `afp/release/thys`
 2.  make sure there is a `thys/entryname/ROOT` file and add `entryname`
     to `thys/ROOTS`. For the former see the template in
     `thys/Example-Submission/ROOT`. In particular the entry should be in
     chapter AFP, and group `(AFP)`, i.e.
 
             chapter AFP
 
             session foo (AFP) = bar +
 
 
 3.  to check, run in `afp/release/thys`
 
          ../admin/testall -c <name>
 
      (be sure to have `ISABELLE_RELEASES` set to the path where Isabelle
     releases are kept, e.g. `/home/proj/isabelle/`)
 4.  check license headers: if the authors want the code released under
     LGPL instead of BSD, each file should mention "License: LGPL" in the
-    header.
+    header. We only accept the BSD 3-Clause and LPGPL version 2.1 licenses
+    as they are printed in `thys/LICENSE` and `thys/LICENSE.LGPL`.
 5.  `hg add` and `hg commit` the new submission
 6.  Enter data for author/abstract/index/etc in the file
     `metadata/metadata`. Make sure that your editor uses UTF-8 encoding
     for this file to preserve special characters. If the entry uses a
     new topic or category, add it to metadata/topics (make sure there is
     an empty line at the end of the file).
 7.  Generate the new web site by running `../admin/sitegen` .
 8.  Use `hg st` and `hg diff` to make sure the generated html makes
     sense. The diff should be small and concern the new entry only.
 9. `hg add` and `hg commit` the web site updates.
 10. finally, when you are happy with everything, `hg push` all changes
-    to bitbucket. The publish script will refuse to publish if the
+    to Heptapod. The publish script will refuse to publish if the
     changes aren't pushed.
 11. to publish the changes to the web, run
 
          ../admin/publish <name>
 
     This will check out the Isabelle202X (=release) version of the
-    archive from bitbucket, will run the session `name` to generate
+    archive from Heptapod, will run the session `name` to generate
     HTML, produce a `.tar.gz` for the archive and for the entry, and
     will update the web pages on the server. The script will ask before
     it copies, so you can check locally if everything is as you want it.
 
 12. That's it. Changes should show up at <http://isa-afp.org>
 
 **New submission in devel**
 
 Although it is a condition of submission that the entry works with the
 current stable Isabelle version, occasionally it happens that a
 submission does not work with the stable version and cannot be
 backported, but is important/good enough to include anyway. In this
 case, we can't release the submission on the main web site yet, but we
 can add it to the development version of the archive, such that it is at
 least available to those who are working with the current Isabelle
 development snapshot.
 
 The check-in procedure is the same as for a normal release entry, apart
 from the fact that everything happens in the devel instead of release
 directory and that the last step (publish) is omitted.
 
 The authors of the entry should be notified that the entry will only
 show up on the front page when the next Isabelle version is released.
diff --git a/doc/maintenance.md b/doc/maintenance.md
--- a/doc/maintenance.md
+++ b/doc/maintenance.md
@@ -1,84 +1,86 @@
 Maintaining an Entry in the AFP
 -------------------------------
 
 To maintain an entry, you must have write access to the mercurial repository
 of the archive at [Heptapod][hetpa]. To get access, [sign up at
 Heptapod][hepta], and ask one of the [editors][editors] to add you to the AFP
 project.
 
 [hepta]: https://foss.heptapod.net
 [editors]: http://isa-afp.org/about.html#editors
 
 **Setup:**
 
  Check out the archive from the mercurial repository with:
 
-    hg clone ssh://hg@bitbucket.org/isa-afp/afp-devel
+    hg clone ssh://hg@foss.heptapod.net/isa-afp/afp-devel
 
 The command above will create a directory `afp-devel` where theories and
 additional files are located. You can register an ssh key for your
-account at Bitbucket under "Manage Account/SSH keys" from the avatar
-icon on the top right of the Bitbucket interface.
+account at Heptapod under "[Settings/SSH keys][keys]" from the avatar
+icon on the top right of the Heptapod interface.
+
+[keys]: https://foss.heptapod.net/profile/keys
 
 **Maintenance:**
 
- Maintaining an entry means making sure that this entry works with the
-current Isabelle development version. Maintainers are not supposed to
-check in and push new entries. New entries must be reviewed and formally
-accepted. They are created on the release branch by the editors.
+Maintaining an entry means making sure that this entry works with the current
+Isabelle development version. Maintainers are not supposed to check in and
+push new entries. New entries must be reviewed and formally accepted. They
+are created on the release branch by the editors.
 
 Depending on the type of the entry, you might want to work in close lock
 step with Isabelle development, i.e. fix the entry immediately each time
 it breaks, or loosely, i.e. only shortly before a new Isabelle release.
 The former is useful for libraries and base entries that are used by
 others, the latter is Ok for larger developments and leaf entries.
 
 Small changes might be done by the Isabelle development team for you as
 the change is introduced to Isabelle (don't be surprised when your entry
 changes slightly over time). You will be notified when an Isabelle
 release nears and your entry is broken. You can also choose to receive
 an automatic email notification each time your entry breaks (see below).
 
 **Technicalities:**
 
 -   To get the current Isabelle development version, use
 
         hg clone http://isabelle.in.tum.de/repos/isabelle
 
     to clone the hg repository. See the README file inside for further
     instructions.
 
 -   Set up your AFP repository as a component by adding
     `init_component "/path_to/afp-devel"` to your
     `~/.isabelle/etc/settings` (or use any other of the component adding
     mechanisms). You need this to get access to the AFP settings and the
     `afp_build` tool.
 -   To check if entry `x` works, execute `isabelle afp_build x`. This
     assumes that the command `isabelle` would start up the current
     Isabelle development version.
 -   To test all entries, run `isabelle afp_build -A`. (Running the
     script with `-?` will show options and usage information)
 -   The changes you make to the mercurial repository will not show up on
     the AFP web pages immediately. This only happens when a new version
     of the archive is released (usually together with Isabelle). Please
     contact one of the editors if you feel there is something that
     should be made available immediately. The changes will show up with
     about 24h delay in the web development snapshot of the AFP.
 -   If you make a change that is more than maintenance and that you
     think may be interesting to users of your entry, please add a manual
     change log in the file `afp-devel/metadata/metadata` by adding an
     `[extra-history]` section to your entry. If possible and sensible,
     this log should link to the relevant hg change set(s). See existing
     change logs like the one for JinjaThreads for examples.
 
 **Email Notification:**
 
  You can receive an automatic email notification if entry `x` breaks by
 editing the file `afp-devel/thys/x/config`:
 
 -   To switch on: add your email address to `NOTIFY`, hg commit, and hg
     push the file. `NOTIFY` is a space separated list. If the entry is
     marked as `FREQUENT`, the test will run daily.
 -   To switch off: remove your email address from `NOTIFY` and hg
     commit + push the file.
 
diff --git a/metadata/templates/about.tpl b/metadata/templates/about.tpl
--- a/metadata/templates/about.tpl
+++ b/metadata/templates/about.tpl
@@ -1,76 +1,76 @@
 {% extends "base.tpl" %}
 
 {% block headline %}
 <font class="first">A</font>rchive of
 <font class="first">F</font>ormal
 <font class="first">P</font>roofs</h1>
 {% endblock %}
 
 {% block content %}
 <table width="80%" class="descr">
   <tbody>
     <tr><td>
 
 <h2>About</h2>
 <p>The Archive of Formal Proofs is a collection of proof libraries, examples,
 and larger scientific developments, mechanically checked in the theorem prover
 <a href="http://isabelle.in.tum.de/">Isabelle</a>. It is organized in the way
 of a scientific journal. <a href="submitting.html">Submissions</a> are
 refereed.</p>
 
-<p>The archive repository is hosted on <a href="https://bitbucket.org">Bitbucket</a> to
+<p>The archive repository is hosted on <a href="https://foss.heptapod.net/isa-afp/">Heptapod</a> to
 provide easy free access to archive entries. The entries are
 tested and maintained continuously against the current stable release of
 Isabelle. Older versions of archive entries will remain available.</p>
 
 <h2>Editors</h2>
 <p><a name="editors">The editors of the archive are</a></p>
 <ul>
 <li><a href="http://www.in.tum.de/~eberlm/">Manuel Eberl</a>,
     <a href="http://www.tum.de/">Technische Universit&auml;t M&uuml;nchen</a></li>
 <li><a href="http://www.cse.unsw.edu.au/~kleing/">Gerwin Klein</a>,
     <a href="http://www.data61.csiro.au">Data61</a></li>
 <li><a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>,
     <a href="http://www.tum.de/">Technische Universit&auml;t M&uuml;nchen</a></li>
 <li><a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>,
     <a href="http://www.cam.ac.uk/">University of Cambridge</a></li>
 <li><a href="http://cl-informatik.uibk.ac.at/users/thiemann/">René Thiemann</a>,
     <a href="https://www.uibk.ac.at/">University of Innsbruck</a></li>
 </ul>
 
 <h2>Why</h2>
 <p>We aim to strengthen the community and to foster the development of formal
 proofs.</p>
 
 <p>We hope that the archive will provide</p>
 <ul>
 <li>a resource of knowledge, examples, and libraries for users,</li>
 <li>a large and relevant test bed of theories for Isabelle developers, and</li>
 <li>a central, citable place for authors to publish their theories</li>
 </ul>
 
 <p>We encourage authors of publications that contain Isabelle developments
 to make their theories available in the Archive of Formal Proofs and to refer
 to the archive entry in their publication. It makes it easier for referees to
 check the validity of theorems (all entries in the archive are
 mechanically checked), it makes it easier for readers of the publication to
 understand details of your development, and it makes it easier to use and
 build on your work.</p>
 
 <h2>License</h2>
-<p>All entries in the Archive of Formal Proofs are licensed under 
+<p>All entries in the Archive of Formal Proofs are licensed under
 a <a href="LICENSE">BSD-style License</a> or
 the <a href="http://www.gnu.org/copyleft/lesser.html">GNU LGPL</a>.
 This means they are free to download, free to use, free to change, and
 free to redistribute with minimal restrictions.</p>
 
 <p>The authors retain their full copyright on their original work,
-including their right to make the development available under another, 
+including their right to make the development available under another,
 additional license in the future.</p>
 
 
     </td></tr>
   </tbody>
 </table>
 {% endblock %}
 
diff --git a/metadata/templates/status.tpl b/metadata/templates/status.tpl
--- a/metadata/templates/status.tpl
+++ b/metadata/templates/status.tpl
@@ -1,62 +1,62 @@
 {% extends "base.tpl" %}
 
 {% block headline %}
 <font class="first">A</font>rchive of
 <font class="first">F</font>ormal
 <font class="first">P</font>roofs
 {% endblock %}
 
 {% block content %}
 <table width="80%" class="entries">
   <tbody>
     <tr><td>
 
 <h3>Test status of entries in the AFP development version</h3>
 <p>
 <table style="margin-left: 30pt;">
 <tbody>
   <tr>
     <td>Isabelle revision:</td>
     <td>
       <a href="http://isabelle.in.tum.de/repos/isabelle/rev/{{ build_data.isabelle_id }}">
         {{ build_data.isabelle_id }}
       </a>
     </td>
   </tr>
   <tr>
     <td>AFP revision:</td>
     <td>
-      <a href="https://bitbucket.org/isa-afp/afp-devel/commits/{{ build_data.afp_id }}">
+      <a href="https://foss.heptapod.net/isa-afp/afp-devel/-/commit/{{ build_data.afp_id }}">
         {{ build_data.afp_id }}
       </a>
     </td>
   </tr>
   <tr><td>Build time:</td><td>{{ build_data.time }}</td></tr>
   <tr><td>Build URL:</td><td><a href="{{ build_data.url }}">Jenkins</a></td></tr>
   <tr><td>Job name:</td><td>{{ build_data.job }}</td></tr>
 </tbody>
 </table>
 </p>
 
     </td></tr>
   </tbody>
 </table>
 
 <p>&nbsp;</p>
 
 <table width="80%" class="entries">
   <tbody>
 
 {% for entry in entries %}
 <tr>
   <td class="status-{{entry.status}}">[{{entry.status}}]</td>
   <td class="entry">
     <a href="entries/{{entry.name}}.html">{{entry.name}}</a>
   </td>
 </tr>
 {% endfor %}
 
   </tbody>
 </table>
 {% endblock %}
 
diff --git a/metadata/templates/submitting.tpl b/metadata/templates/submitting.tpl
--- a/metadata/templates/submitting.tpl
+++ b/metadata/templates/submitting.tpl
@@ -1,87 +1,87 @@
 {% extends "base.tpl" %}
 
 {% block headline %}
 <font class="first">S</font>ubmission
 <font class="first">G</font>uidelines
 {% endblock %}
 
 {% block content %}
 <table width="80%" class="descr">
   <tbody>
     <tr><td>
 
 <p>Please send your submission
 <a href="https://ci.isabelle.systems/afp-submission/">via this web page</a>.
 </p>
 
 <p><strong>The submission must follow the following Isabelle style rules.</strong>
     For additional guidelines on Isabelle proofs, also see the this <a href="http://proofcraft.org/blog/isabelle-style.html">guide</a> (feel free to follow all of these; only the below are mandatory).
     <strong>Technical details about the submission process and the format of the submission are explained on the submission site.</strong></p>
 <ul>
     <li>No use of the commands <code>sorry</code> or <code>back</code>.</li>
 
     <li>Instantiations must not use Isabelle-generated names such as
     <code>xa</code> &mdash; use Isar, the <code>subgoal</code> command
     or <code>rename_tac</code> to avoid such names.</li>
 
     <li>No use of the command <code>smt_oracle</code>.</li>
 
     <li>If your theories contain calls to <code>nitpick</code>,
     <code>quickcheck</code>, or <code>nunchaku</code> those calls must
     include the <code>expect</code> parameter. Alternatively the
     <code>expect</code> parameter must be set globally via, e.g.
     <code>nitpick_params</code>.</li>
 
     <li><code>apply</code> scripts should be indented by subgoal as in
     the Isabelle distribution. If an <code>apply</code> command is
     applied to a state with <code>n+1</code> subgoals, it must be
     indented by <code>n</code> spaces relative to the first
     <code>apply</code> in the sequence.</li>
 
     <li>Only named lemmas should carry attributes such as <code>[simp]</code>.</li>
 
     <li>We prefer structured Isar proofs over apply style, but do not
     mandate them.</li>
 
     <li>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.</li>
 
     <li>The entry must contain a ROOT file with one session that has the
         name of the entry. We strongly encourage precisely one session per
         entry, but exceptions can be made. All sessions must be in group
         (AFP), and all theory files of the submission must be contained in
-        at least one session. See also the example <a href="https://bitbucket.org/isa-afp/afp-2018/src/default/thys/Example-Submission/ROOT">ROOT</a> file
+        at least one session. See also the example <a href="https://foss.heptapod.net/isa-afp/afp-2020/-/blob/branch/default/thys/Example-Submission/ROOT">ROOT</a> file
         in the <a href="entries/Example-Submission.html">Example submission</a>.
 	</li>
 
     <li>The entry should cite all sources that the theories are based on,
     for example textbooks or research articles containing informal versions of the proofs.</li>
 </ul>
 
 <p>Your submission must contain an abstract to be displayed on the web site &ndash; usually this will be the same as the abstract of your proof document in the <tt>root.tex</tt> file. You can use LaTeX formulae in this web site abstract, either inline formulae in the form <tt>$a+b$</tt> or <tt>\(a+b\)</tt> or display formulae in the form <tt>$$a + b$$</tt> or <tt>\[a + b\]</tt>. Other occurrences of these characters must be escaped (e.g. <tt>\$</tt> or <tt>\\(</tt>). Note that LaTeX in the title of an entry is <em>not</em> allowed. Most basic LaTeX functionality should be supported. For details on what parts of LaTeX are supported, see the <a href="https://docs.mathjax.org/en/v2.7-latest/tex.html">MathJax documentation.</a></p>
 
 <p>It is possible and encouraged to build on other archive entries
    in your submission. There is a standardised way to
    <a href="using.html">refer to other AFP entries</a> in your
    theories.</p>
 
 <p>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.</p>
 
 <p>If you have questions regarding your submission, please email <a
 href="&#109;&#97;&#105;&#108;&#116;&#111;:&#97;&#102;&#112;-&#115;&#117;&#98;&#109;&#105;&#116;&#64;&#105;&#110;&#46;&#116;&#117;&#109;&#46;&#100;&#101;">&#97;&#102;&#112;-&#115;&#117;&#98;&#109;&#105;&#116;&#64;&#105;&#110;&#46;&#116;&#117;&#109;&#46;&#100;&#101;</a>.
       If you need help with Isabelle, please use the
 <a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
       mailing list. It is always a good idea to <a
       href="https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users">subscribe</a>.</p>
 
     </td></tr>
   </tbody>
 </table>
 
 {% endblock %}
 
diff --git a/metadata/templates/updating.tpl b/metadata/templates/updating.tpl
--- a/metadata/templates/updating.tpl
+++ b/metadata/templates/updating.tpl
@@ -1,102 +1,102 @@
 {% extends "base.tpl" %}
 
 {% block headline %}
 <font class="first">U</font>pdating
 <font class="first">E</font>ntries
 {% endblock %}
 
 {% block content %}
 <table width="80%" class="descr">
   <tbody>
     <tr><td>
 
 <h2>Change</h2>
 <p>
 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
 authors.
 </p>
 <p>
 This conflicts with the purpose of archiving and preserving
-entries as they have been submitted and with the purpose of 
+entries as they have been submitted and with the purpose of
 providing a clear and simple interface to readers.
 </p>
 <p>
 The AFP deals with this by synchronizing such updates with
 Isabelle releases:
 </p>
 <ul>
 <li>
 The entries released and visible on the main site are always
 working with the most recent stable Isabelle version and do not
 change.
 </li>
 <li>
 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 <a
-href="https://bitbucket.org/isa-afp/afp-devel/">bitbucket
+href="https://foss.heptapod.net/isa-afp/afp-devel/">Heptapod
 mercurial repository</a> or as tar.gz package on the <a href="download.html">
 download page</a>.
 </li>
 <li>
 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
 accessible.
 </li>
 </ul>
 
 <p>
 Significant changes of an entry should be recorded in the metadata of the
 entry using the keyword "extra-history". The resulting web page should look
 <a href="https://www.isa-afp.org/entries/JinjaThreads.html">something like this</a>.
 </p>
 
 <h2>Monotonicity</h2>
 
 <p>
 Updating an entry should be mostly monotone: you add new material, but you do
 not modify existing material in a major way. Ideally, entries (by other
 people) that build on yours should not be affected. Otherwise you have to
 liaise with them first. If you intend to carry out major non-monotone
 changes, you will need to submit a completely new entry (with a description
 of how it relates to the old one). This should be required only very rarely:
 AFP entries should be mature enough not to require major changes to their
 interface (i.e. the main functions and theorems provided).
 </p>
 
 <p>
 Major monotone changes, e.g. adding a new concept rather than more results on
 existing concepts, may also call for a new entry, but one that builds on the
 existing one. This depends on how you would like to organize your entries.
 </p>
 
 <h2>If you are an author</h2>
 
 <p>
 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.
 </p>
 <p>
 To achieve this, you should base your changes on the <a
-href="https://bitbucket.org/isa-afp/afp-devel/">mercurial 
+href="https:/foss.heptapod.net/isa-afp/afp-devel/">mercurial
 development version</a>
 of your AFP entry and test it against the current <a
 href="http://isabelle.in.tum.de/devel/">Isabelle development
 version</a>.
 </p>
 <p>
-If you would like to get write access to your entry in the 
+If you would like to get write access to your entry in the
 mercurial repository or if you need
 assistance, please contact the <a href="about.html#editors">editors</a>.
 </p>
 
     </td></tr>
   </tbody>
 </table>
 {% endblock %}
 
diff --git a/web/about.html b/web/about.html
--- a/web/about.html
+++ b/web/about.html
@@ -1,144 +1,144 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
 <meta charset="utf-8">
 <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">
 <link rel="alternate" type="application/rss+xml" title="RSS" href="rss.xml">
  </head>
 
 <body class="mathjax_ignore">
 
 <table width="100%">
 <tbody>
 <tr>
 
 <!-- Navigation -->
 <td width="20%" align="center" valign="top">
   <p>&nbsp;</p>
   <a href="https://www.isa-afp.org/">
     <img src="images/isabelle.png" width="100" height="88" border=0>
   </a>
   <p>&nbsp;</p>
   <p>&nbsp;</p>
   <table class="nav" width="80%">
     <tr>
       <td class="nav" width="100%"><a href="index.html">Home</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="about.html">About</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="submitting.html">Submission</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="updating.html">Updating Entries</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="using.html">Using Entries</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="search.html">Search</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="statistics.html">Statistics</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="topics.html">Index</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="download.html">Download</a></td>
     </tr>
   </table>
   <p>&nbsp;</p>
   <p>&nbsp;</p>
 </td>
 
 
 <!-- Content -->
 <td width="80%" valign="top">
 <div align="center">
   <p>&nbsp;</p>
   <h1><font class="first">A</font>rchive of
 <font class="first">F</font>ormal
 <font class="first">P</font>roofs</h1>
 </h1>
   <p>&nbsp;</p>
 
 <table width="80%" class="descr">
   <tbody>
     <tr><td>
 
 <h2>About</h2>
 <p>The Archive of Formal Proofs is a collection of proof libraries, examples,
 and larger scientific developments, mechanically checked in the theorem prover
 <a href="http://isabelle.in.tum.de/">Isabelle</a>. It is organized in the way
 of a scientific journal. <a href="submitting.html">Submissions</a> are
 refereed.</p>
 
-<p>The archive repository is hosted on <a href="https://bitbucket.org">Bitbucket</a> to
+<p>The archive repository is hosted on <a href="https://foss.heptapod.net/isa-afp/">Heptapod</a> to
 provide easy free access to archive entries. The entries are
 tested and maintained continuously against the current stable release of
 Isabelle. Older versions of archive entries will remain available.</p>
 
 <h2>Editors</h2>
 <p><a name="editors">The editors of the archive are</a></p>
 <ul>
 <li><a href="http://www.in.tum.de/~eberlm/">Manuel Eberl</a>,
     <a href="http://www.tum.de/">Technische Universit&auml;t M&uuml;nchen</a></li>
 <li><a href="http://www.cse.unsw.edu.au/~kleing/">Gerwin Klein</a>,
     <a href="http://www.data61.csiro.au">Data61</a></li>
 <li><a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>,
     <a href="http://www.tum.de/">Technische Universit&auml;t M&uuml;nchen</a></li>
 <li><a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>,
     <a href="http://www.cam.ac.uk/">University of Cambridge</a></li>
 <li><a href="http://cl-informatik.uibk.ac.at/users/thiemann/">René Thiemann</a>,
     <a href="https://www.uibk.ac.at/">University of Innsbruck</a></li>
 </ul>
 
 <h2>Why</h2>
 <p>We aim to strengthen the community and to foster the development of formal
 proofs.</p>
 
 <p>We hope that the archive will provide</p>
 <ul>
 <li>a resource of knowledge, examples, and libraries for users,</li>
 <li>a large and relevant test bed of theories for Isabelle developers, and</li>
 <li>a central, citable place for authors to publish their theories</li>
 </ul>
 
 <p>We encourage authors of publications that contain Isabelle developments
 to make their theories available in the Archive of Formal Proofs and to refer
 to the archive entry in their publication. It makes it easier for referees to
 check the validity of theorems (all entries in the archive are
 mechanically checked), it makes it easier for readers of the publication to
 understand details of your development, and it makes it easier to use and
 build on your work.</p>
 
 <h2>License</h2>
-<p>All entries in the Archive of Formal Proofs are licensed under 
+<p>All entries in the Archive of Formal Proofs are licensed under
 a <a href="LICENSE">BSD-style License</a> or
 the <a href="http://www.gnu.org/copyleft/lesser.html">GNU LGPL</a>.
 This means they are free to download, free to use, free to change, and
 free to redistribute with minimal restrictions.</p>
 
 <p>The authors retain their full copyright on their original work,
-including their right to make the development available under another, 
+including their right to make the development available under another,
 additional license in the future.</p>
 
 
     </td></tr>
   </tbody>
 </table>
 
 </div>
 </td>
 
 </tr>
 </tbody>
 </table>
 
 
 </body>
 </html>
\ No newline at end of file
diff --git a/web/statistics.html b/web/statistics.html
--- a/web/statistics.html
+++ b/web/statistics.html
@@ -1,307 +1,307 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
 <meta charset="utf-8">
 <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">
 <link rel="alternate" type="application/rss+xml" title="RSS" href="rss.xml">
  </head>
 
 <body class="mathjax_ignore">
 
 <table width="100%">
 <tbody>
 <tr>
 
 <!-- Navigation -->
 <td width="20%" align="center" valign="top">
   <p>&nbsp;</p>
   <a href="https://www.isa-afp.org/">
     <img src="images/isabelle.png" width="100" height="88" border=0>
   </a>
   <p>&nbsp;</p>
   <p>&nbsp;</p>
   <table class="nav" width="80%">
     <tr>
       <td class="nav" width="100%"><a href="index.html">Home</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="about.html">About</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="submitting.html">Submission</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="updating.html">Updating Entries</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="using.html">Using Entries</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="search.html">Search</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="statistics.html">Statistics</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="topics.html">Index</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="download.html">Download</a></td>
     </tr>
   </table>
   <p>&nbsp;</p>
   <p>&nbsp;</p>
 </td>
 
 
 <!-- Content -->
 <td width="80%" valign="top">
 <div align="center">
   <p>&nbsp;</p>
   <h1><font class="first">S</font>tatistics
 </h1>
   <p>&nbsp;</p>
 
 <table width="80%" class="descr">
   <tbody>
     <tr><td>
       <h2>Statistics</h2>
 
 <table>
 <tr><td>Number of Articles:</td><td class="statsnumber">545</td></tr>
 <tr><td>Number of Authors:</td><td class="statsnumber">359</td></tr>
 <tr><td>Number of lemmas:</td><td class="statsnumber">~147,800</td></tr>
-<tr><td>Lines of Code:</td><td class="statsnumber">~2,571,700</td></tr>
+<tr><td>Lines of Code:</td><td class="statsnumber">~2,571,600</td></tr>
 </table>
 <h4>Most used AFP articles:</h4>
 <table id="most_used">
 <tr>
 <th></th><th>Name</th><th>Used by ? articles</th>
 </tr>
 
   <tr><td>1.</td>
         
     <td><a href="entries/List-Index.html">List-Index</a></td>
     <td>15</td>
     </tr>
     <tr><td>2.</td>
         
     <td><a href="entries/Coinductive.html">Coinductive</a></td>
     <td>12</td>
     </tr>
       <td></td>
     <td><a href="entries/Collections.html">Collections</a></td>
     <td>12</td>
     </tr>
       <td></td>
     <td><a href="entries/Regular-Sets.html">Regular-Sets</a></td>
     <td>12</td>
     </tr>
     <tr><td>3.</td>
         
     <td><a href="entries/Landau_Symbols.html">Landau_Symbols</a></td>
     <td>11</td>
     </tr>
     <tr><td>4.</td>
         
     <td><a href="entries/Show.html">Show</a></td>
     <td>10</td>
     </tr>
     <tr><td>5.</td>
         
     <td><a href="entries/Abstract-Rewriting.html">Abstract-Rewriting</a></td>
     <td>9</td>
     </tr>
       <td></td>
     <td><a href="entries/Automatic_Refinement.html">Automatic_Refinement</a></td>
     <td>9</td>
     </tr>
       <td></td>
     <td><a href="entries/Deriving.html">Deriving</a></td>
     <td>9</td>
     </tr>
       <td></td>
     <td><a href="entries/Polynomial_Factorization.html">Polynomial_Factorization</a></td>
     <td>9</td>
     </tr>
     <tr><td>6.</td>
         
     <td><a href="entries/Jordan_Normal_Form.html">Jordan_Normal_Form</a></td>
     <td>8</td>
     </tr>
       <td></td>
     <td><a href="entries/Native_Word.html">Native_Word</a></td>
     <td>8</td>
     </tr>
   
 </table>
 <script>
 // DATA
 var years = [2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2020];
 var no_articles = [14, 22, 29, 37, 52, 64, 86, 103, 128, 151, 208, 253, 326, 396, 455, 511, 545];
-var no_loc = [61000.0, 96800.0, 131400.0, 238800.0, 353700.0, 435900.0, 517100.0, 568100.0, 740400.0, 828300.0, 1038400.0, 1216700.0, 1581000.0, 1830700.0, 2104700.0, 2399200.0, 2571700.0 ];
+var no_loc = [61000.0, 96800.0, 131400.0, 238800.0, 353700.0, 435900.0, 517100.0, 568100.0, 740400.0, 828300.0, 1038400.0, 1216700.0, 1581000.0, 1830600.0, 2104700.0, 2399200.0, 2571600.0 ];
 var no_authors = [14, 11, 6, 6, 10, 6, 24, 11, 17, 16, 36, 20, 63, 31, 28, 38, 22];
 var no_authors_series = [14, 25, 31, 37, 47, 53, 77, 88, 105, 121, 157, 177, 240, 271, 299, 337, 359];
 var all_articles = [ "MiniML","AVL-Trees","Functional-Automata","BinarySearchTree","Lazy-Lists-II","Topology","Group-Ring-Module","Depth-First-Search","Compiling-Exceptions-Correctly","Completeness","Ramsey-Infinite","Verified-Prover","Integration","FileRefinement","Category","RSAPSS","Jinja","JiveDataStoreModel","DiskPaxos","GenClock","FFT","Ordinal","Cauchy","ClockSynchInst","FeatherweightJava","CoreC++","Flyspeck-Tame","Abstract-Hoare-Logics","HotelKeyCards","FOL-Fitting","POPLmark-deBruijn","Valuation","SumSquares","Fermat3_4","MuchAdoAboutTwo","JinjaThreads","Program-Conflict-Analysis","LinearQuantifierElim","NormByEval","Simpl","BDD","Recursion-Theory-I","SATSolverVerification","FunWithFunctions","ArrowImpossibilityGS","VolpanoSmith","Slicing","Huffman","FunWithTilings","SenSocialChoice","SIFPL","BytecodeLogicJmlTypes","Stream-Fusion","FinFun","CofGroups","SequentInvertibility","Ordinals_and_Cardinals","WorkerWrapper","HRB-Slicing","Perfect-Number-Thm","Collections","Tree-Automata","Presburger-Automata","DPT-SAT-Solver","Coinductive","List-Index","InformationFlowSlicing","InformationFlowSlicing_Inter","Free-Boolean-Algebra","Locally-Nameless-Sigma","Regular-Sets","Robbins-Conjecture","DataRefinementIBP","GraphMarkingIBP","Abstract-Rewriting","Matrix","Category2","Free-Groups","Statecharts","Polynomials","Lam-ml-Normalization","Binomial-Queues","Binomial-Heaps","Finger-Trees","Shivers-CFA","Marriage","Lower_Semicontinuous","RIPEMD-160-SPARK","LightweightJava","List-Infinite","AutoFocus-Stream","Nat-Interval-Logic","Transitive-Closure","General-Triangle","KBPs","Max-Card-Matching","Gauss-Jordan-Elim-Fun","Myhill-Nerode","LatticeProperties","MonoBoolTranAlgebra","PseudoHoops","Efficient-Mergesort","TLA","Markov_Models","Dijkstra_Shortest_Path","Refine_Monadic","Girth_Chromatic","Transitive-Closure-II","Abortable_Linearizable_Modules","Well_Quasi_Orders","Ordinary_Differential_Equations","Inductive_Confidentiality","Stuttering_Equivalence","Separation_Algebra","Circus","Psi_Calculi","CCS","Pi_Calculus","Tycon","PCF","Heard_Of","Impossible_Geometry","Datatype_Order_Generator","Possibilistic_Noninterference","Bondy","Tarskis_Geometry","Open_Induction","Separation_Logic_Imperative_HOL","Sqrt_Babylonian","Kleene_Algebra","Rank_Nullity_Theorem","Ribbon_Proofs","Launchbury","Nominal2","Containers","Graph_Theory","ShortestPath","Sort_Encodings","Koenigsberg_Friendship","Lehmer","Pratt_Certificate","IEEE_Floating_Point","Native_Word","Automatic_Refinement","Decreasing-Diagrams","GoedelGod","FocusStreamsCaseStudies","Coinductive_Languages","Incompleteness","HereditarilyFinite","Tail_Recursive_Functions","CryptoBasedCompositionalProperties","Sturm_Sequences","Featherweight_OCL","KAT_and_DRA","Relation_Algebra","Secondary_Sylow","Regex_Equivalence","Real_Impl","Affine_Arithmetic","Selection_Heap_Sort","Random_Graph_Subgraph_Threshold","Partial_Function_MR","AWN","Probabilistic_Noninterference","GPU_Kernel_PL","Discrete_Summation","HyperCTL","Abstract_Completeness","Bounded_Deducibility_Security","SIFUM_Type_Systems","WHATandWHERE_Security","Strong_Security","ComponentDependencies","Regular_Algebras","Noninterference_CSP","Roy_Floyd_Warshall","Gabow_SCC","CAVA_Automata","CAVA_LTL_Modelchecker","LTL_to_GBA","Promela","Boolean_Expression_Checkers","MSO_Regex_Equivalence","Pop_Refinement","Network_Security_Policy_Verification","Amortized_Complexity","pGCL","CISC-Kernel","Show","Splay_Tree","Skew_Heap","VectorSpace","Special_Function_Bounds","Gauss_Jordan","Priority_Queue_Braun","Jordan_Hoelder","Cayley_Hamilton","Sturm_Tarski","Imperative_Insertion_Sort","Certification_Monads","XML","RefinementReactive","Density_Compiler","Stream_Fusion_Code","Lifting_Definition_Option","AODV","UPF","UpDown_Scheme","Finite_Automata_HF","QR_Decomposition","Echelon_Form","Call_Arity","Deriving","Consensus_Refined","Trie","ConcurrentIMP","ConcurrentGC","Residuated_Lattices","Vickrey_Clarke_Groves","Probabilistic_System_Zoo","Formula_Derivatives","Dynamic_Tables","Noninterference_Ipurge_Unwinding","Noninterference_Generic_Unwinding","List_Interleaving","Multirelations","Derangements","Hermite","Akra_Bazzi","Landau_Symbols","Case_Labeling","Encodability_Process_Calculi","Rep_Fin_Groups","Noninterference_Inductive_Unwinding","Decreasing-Diagrams-II","Jordan_Normal_Form","LTL_to_DRA","Isabelle_Meta_Model","Parity_Game","Planarity_Certificates","TortoiseHare","Euler_Partition","Ergodic_Theory","Latin_Square","Card_Partitions","Applicative_Lifting","Algebraic_Numbers","Stern_Brocot","Liouville_Numbers","Triangle","Prime_Harmonic_Series","Descartes_Sign_Rule","Card_Number_Partitions","Matrix_Tensor","Knot_Theory","Polynomial_Factorization","Polynomial_Interpolation","Formal_SSA","List_Update","LTL","Cartan_FP","Timed_Automata","PropResPI","KAD","Noninterference_Sequential_Composition","ROBDD","CYK","No_FTL_observers","Groebner_Bases","Bell_Numbers_Spivey","SDS_Impossibility","Randomised_Social_Choice","MFMC_Countable","FLP","Perron_Frobenius","Incredible_Proof_Machine","Posix-Lexing","Card_Equiv_Relations","Tree_Decomposition","Word_Lib","Noninterference_Concurrent_Composition","Algebraic_VCs","Catalan_Numbers","Dependent_SIFUM_Type_Systems","Card_Multisets","Category3","Dependent_SIFUM_Refinement","IP_Addresses","Rewriting_Z","Resolution_FOL","Buildings","DFS_Framework","Pairing_Heap","Surprise_Paradox","Ptolemys_Theorem","Refine_Imperative_HOL","EdmondsKarp_Maxflow","InfPathElimination","Simple_Firewall","Routing","Stirling_Formula","Stone_Algebras","SuperCalc","Iptables_Semantics","Lambda_Free_RPOs","Allen_Calculus","Fisher_Yates","Lp","Chord_Segments","Berlekamp_Zassenhaus","Source_Coding_Theorem","SPARCv8","LOFT","Stable_Matching","Modal_Logics_for_NTS","Deep_Learning","Lambda_Free_KBOs","Nested_Multisets_Ordinals","Separata","Abs_Int_ITP2012","Complx","Paraconsistency","Proof_Strategy_Language","Twelvefold_Way","Concurrent_Ref_Alg","FOL_Harrison","Password_Authentication_Protocol","UPF_Firewall","E_Transcendental","Bertrands_Postulate","Minimal_SSA","Bernoulli","Key_Agreement_Strong_Adversaries","Stone_Relation_Algebras","Abstract_Soundness","Differential_Dynamic_Logic","Menger","Elliptic_Curves_Group_Law","Euler_MacLaurin","Quick_Sort_Cost","Comparison_Sort_Lower_Bound","Random_BSTs","Subresultants","Lazy_Case","Constructor_Funs","LocalLexing","Types_Tableaus_and_Goedels_God","MonoidalCategory","Game_Based_Crypto","Monomorphic_Monad","Probabilistic_While","Monad_Normalisation","CryptHOL","Floyd_Warshall","Security_Protocol_Refinement","Dict_Construction","Optics","Flow_Networks","Prpu_Maxflow","Buffons_Needle","PSemigroupsConvolution","Propositional_Proof_Systems","Stone_Kleene_Relation_Algebras","CRDT","Name_Carrying_Type_Inference","Minkowskis_Theorem","HOLCF-Prelude","Decl_Sem_Fun_PL","DynamicArchitectures","Stewart_Apollonius","LambdaMu","Orbit_Stabiliser","Root_Balanced_Tree","First_Welfare_Theorem","AnselmGod","PLM","Lowe_Ontological_Argument","Dirichlet_Series","Zeta_Function","Linear_Recurrences","Diophantine_Eqns_Lin_Hom","Winding_Number_Eval","Count_Complex_Roots","Buchi_Complementation","Transition_Systems_and_Automata","Kuratowski_Closure_Complement","Hybrid_Multi_Lane_Spatial_Logic","IMAP-CRDT","Stochastic_Matrices","Knuth_Morris_Pratt","BNF_Operations","Dirichlet_L","Mason_Stothers","Median_Of_Medians_Selection","Falling_Factorial_Sum","Taylor_Models","Green","Gromov_Hyperbolicity","Ordered_Resolution_Prover","LLL_Basis_Reduction","Treaps","First_Order_Terms","Error_Function","LLL_Factorization","Hoare_Time","Architectural_Design_Patterns","CakeML","Weight_Balanced_Trees","Fishburn_Impossibility","BNF_CC","VerifyThis2018","WebAssembly","Modular_Assembly_Kit_Security","OpSets","Monad_Memo_DP","AxiomaticCategoryTheory","Irrationality_J_Hancl","Probabilistic_Timed_Automata","Hidden_Markov_Models","Optimal_BST","Partial_Order_Reduction","Projective_Geometry","Localization_Ring","Pell","Neumann_Morgenstern_Utility","DiscretePricing","Minsky_Machines","Simplex","Budan_Fourier","Quaternions","Octonions","Aggregation_Algebras","Prime_Number_Theorem","Signature_Groebner","Symmetric_Polynomials","Pi_Transcendental","Factored_Transition_System_Bounding","Randomised_BSTs","Lambda_Free_EPO","Smooth_Manifolds","Epistemic_Logic","GewirthPGCProof","Generic_Deriving","Matroids","Auto2_HOL","Functional_Ordered_Resolution_Prover","Graph_Saturation","Transformer_Semantics","Order_Lattice_Props","Quantales","Constructive_Cryptography","Auto2_Imperative_HOL","Concurrent_Revisions","Core_DOM","Store_Buffer_Reduction","Higher_Order_Terms","IMP2","Farkas","List_Inversions","UTP","Universal_Turing_Machine","Probabilistic_Prime_Tests","Kruskal","Prime_Distribution_Elementary","Safe_OCL","QHLProver","Transcendence_Series_Hancl_Rucki","Binding_Syntax_Theory","LTL_Master_Theorem","HOL-CSP","Multi_Party_Computation","LambdaAuth","KD_Tree","Differential_Game_Logic","IMP2_Binary_Heap","Groebner_Macaulay","Nullstellensatz","Linear_Inequalities","Priority_Search_Trees","Prim_Dijkstra_Simple","Complete_Non_Orders","MFOTL_Monitor","CakeML_Codegen","FOL_Seq_Calc1","Szpilrajn","TESL_Language","Stellar_Quorums","IMO2019","C2KA_DistributedSystems","Linear_Programming","Laplace_Transform","Adaptive_State_Counting","Jacobson_Basic_Algebra","Fourier","Hybrid_Systems_VCs","Generic_Join","Clean","Sigma_Commit_Crypto","Aristotles_Assertoric_Syllogistic","VerifyThis2019","Isabelle_C","ZFC_in_HOL","Interval_Arithmetic_Word32","Generalized_Counting_Sort","Gauss_Sums","Poincare_Disc","Complex_Geometry","Poincare_Bendixson","Hybrid_Logic","Zeta_3_Irrational","Bicategory","Skip_Lists","Closest_Pair_Points","Approximation_Algorithms","Mersenne_Primes","Subset_Boolean_Algebras","Arith_Prog_Rel_Primes","VeriComp","Goodstein_Lambda","Hello_World","Relational-Incorrectness-Logic","Furstenberg_Topology","WOOT_Strong_Eventual_Consistency","Lucas_Theorem","Automated_Stateful_Protocol_Verification","Stateful_Protocol_Composition_and_Typing","MFODL_Monitor_Optimized","Saturation_Framework","Sliding_Window_Algorithm","ADS_Functor","Matrices_for_ODEs","Power_Sum_Polynomials","Lambert_W","Gaussian_Integers","Attack_Trees","Banach_Steinhaus","Forcing","LTL_Normal_Form","Recursion-Addition","Irrational_Series_Erdos_Straus","Knuth_Bendix_Order","Nash_Williams","Smith_Normal_Form","Safe_Distance"];
 var years_loc_articles = [  2004        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2005        ,    ,    ,    ,    ,    ,    ,  ,2006        ,    ,    ,    ,    ,    ,  ,2007        ,    ,    ,    ,    ,    ,    ,  ,2008        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2009        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2010        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2011        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2012        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2013        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2014        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2015        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2016        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2017        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2018        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2019        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,  ,2020        ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,    ,];
-var loc_articles = [ "1825","839","1544","1096","1058","2419","44269","205","142","1994","209","1109","3792","506","1141","3769","17207","3119","6430","1145","447","2537","1275","1583","1838","12833","13115","2685","1228","3556","4238","9649","970","2847","1741","79735","4738","3396","2186","31192","10664","6723","30332","180","793","1047","14413","2080","254","2221","5958","3458","799","1540","684","6654","8","2627","27490","330","32400","5025","4380","210","9533","447","2380","3399","611","6311","2042","840","713","1024","5632","1427","4078","2230","6061","22617","1602","1587","3370","2449","2592","260","1621","16","2930","7805","6557","6381","992","125","10136","332","235","1828","1039","1784","4425","303","4461","11857","2834","8582","1043","408","2940","2613","38074","3243","1480","2611","3153","27588","2580","25275","2266","4107","7701","1245","260","5309","73","9729","719","6673","1511","4354","1249","1908","6215","4974","10067","7894","538","3830","4595","202","848","1774","5466","10327","1524","150","5292","706","10774","2248","1458","1958","3067","11485","1860","1190","1219","2175","1144","14861","2215","1964","166","10685","6420","572","590","1698","465","883","4133","2138","1403","2280","1959","2467","220","5432","4431","9390","3999","4463","406","5935","1829","12828","2973","9486","4560","931","645","104","2338","1653","9143","752","2113","875","1727","627","931","1201","1296","7880","1922","90","28055","2879","2796","1116","4863","5259","8842","1169","6178","527","1601","6194","1782","5327","1085","4103","952","2446","1089","1060","2362","468","2074","3761","2148","710","16080","8267","908","1063","21109","9679","8653","3142","9161","695","435","13711","478","898","2716","10063","1162","401","498","495","741","843","3622","4616","6228","4123","8166","12108","3178","518","17583","2876","2411","5496","2453","886","1162","17386","509","702","5036","9700","4287","5331","3811","656","329","1057","8295","3257","2593","553","8478","206","17950","8773","3278","398","2960","12833","9483","373","173","384","18976","2545","6119","3779","1017","2608","4338","9356","20041","4053","3420","319","3204","169","19538","541","14628","2648","7056","7590","3898","3244","4546","855","2289","5001","1349","276","4339","1475","3482","7114","9662","601","1722","852","2194","12220","4116","590","13558","1695","4484","1640","835","694","737","3346","105","68","10492","1127","8000","4135","4711","1200","378","9435","2078","14059","639","2015","3930","4869","398","1531","5554","5614","1991","4205","478","4121","3146","3471","88","480","1261","1877","2193","250","10669","854","7463","5301","3079","2808","8849","5261","2326","6172","945","6514","992","489","809","8891","3133","338","854","493","4585","9457","15962","6326","10249","1818","2288","785","3260","8438","3278","12949","592","841","3383","3642","11559","13548","3734","5742","530","1044","7674","1042","1259","5297","2754","1390","1622","2173","13358","805","10028","2667","541","1271","3955","5318","9770","2765","934","11918","1743","2355","7917","1490","449","685","1811","1132","3540","3578","1644","2983","2218","7221","4968","2767","16972","34365","3259","6022","1900","372","10332","16867","3018","3300","5304","4576","10486","1000","15843","4437","9487","5543","3300","1264","2973","805","10253","2606","5262","472","3365","1869","2599","13350","945","192","4455","527","713","782","2335","2134","9934","2089","3736","3105","2350","3195","3812","176","1726","8509","6804","4836","5723","4561","10314","14530","6402","4470","1907","51409","2450","3936","2758","1699","3154","944","906","596","375","691","766","2564","332","14517","21769","11317","3074","744","2351","1559","1239","1609","2537","1939","1341","12003","1034","1444","1938","2670","827","12969","3025"];
+var loc_articles = [ "1825","839","1544","1096","1058","2419","44269","205","142","1994","209","1109","3792","506","1141","3769","17207","3119","6430","1145","447","2537","1275","1583","1838","12833","13115","2685","1228","3556","4238","9649","970","2847","1741","79735","4738","3396","2186","31192","10664","6723","30332","180","793","1047","14413","2080","254","2221","5958","3458","799","1540","684","6654","8","2627","27490","330","32400","5025","4380","210","9533","447","2380","3399","611","6311","2042","840","713","1024","5632","1427","4078","2230","6061","22617","1602","1587","3370","2449","2592","260","1621","16","2930","7805","6557","6381","992","125","10136","332","235","1828","1039","1784","4425","303","4461","11857","2834","8582","1043","408","2940","2613","38074","3243","1480","2611","3153","27588","2580","25275","2266","4107","7701","1245","260","5309","73","9729","719","6673","1511","4354","1249","1908","6215","4974","10067","7894","538","3830","4595","202","848","1774","5466","10327","1524","150","5292","706","10774","2248","1458","1958","3067","11485","1860","1190","1219","2175","1144","14861","2215","1964","166","10685","6420","572","590","1698","465","883","4133","2138","1403","2280","1959","2467","220","5432","4431","9390","3999","4463","406","5935","1829","12828","2973","9486","4560","931","645","104","2338","1653","9143","752","2113","875","1727","627","931","1201","1296","7880","1922","90","28055","2879","2796","1116","4863","5259","8842","1169","6178","527","1601","6194","1782","5327","1085","4103","952","2446","1089","1060","2362","468","2074","3761","2148","710","16080","8267","908","1063","21109","9679","8653","3142","9161","695","435","13711","478","898","2716","10063","1162","401","498","495","741","843","3622","4616","6228","4123","8166","12108","3178","518","17583","2876","2411","5496","2453","886","1162","17386","509","702","5036","9700","4287","5331","3811","656","329","1057","8295","3257","2593","553","8478","206","17950","8773","3278","398","2960","12833","9483","373","173","384","18976","2545","6119","3779","1017","2608","4338","9356","20041","4053","3420","319","3204","169","19538","541","14628","2648","7056","7590","3898","3244","4546","855","2289","5001","1349","276","4339","1475","3482","7114","9662","601","1722","852","2194","12220","4116","590","13558","1695","4484","1640","835","694","737","3346","105","68","10492","1127","8000","4135","4711","1200","378","9435","2078","14059","639","2015","3930","4869","398","1531","5554","5614","1991","4205","478","4121","3146","3471","88","480","1261","1877","2193","250","10669","854","7463","5301","3079","2808","8849","5261","2325","6164","945","6514","992","489","809","8891","3133","338","854","493","4585","9457","15962","6326","10249","1818","2288","785","3260","8438","3278","12949","592","841","3383","3642","11559","13548","3734","5742","530","1044","7674","1042","1259","5297","2754","1390","1622","2173","13358","805","10026","2667","541","1271","3955","5318","9770","2765","934","11918","1743","2355","7917","1490","449","685","1811","1132","3540","3578","1644","2983","2218","7221","4968","2767","16972","34365","3259","6022","1900","372","10332","16867","3018","3300","5304","4576","10486","1000","15843","4437","9487","5543","3300","1264","2973","805","10253","2606","5262","472","3365","1869","2599","13350","945","192","4455","527","713","782","2335","2134","9934","2089","3736","3105","2350","3195","3812","176","1726","8509","6804","4836","5723","4561","10314","14530","6402","4470","1907","51409","2450","3936","2758","1699","3154","944","906","596","375","691","766","2564","332","14517","21769","11317","3074","744","2351","1559","1239","1609","2537","1939","1341","12003","1034","1444","1938","2670","827","12968","3025"];
 
 </script>
 <h4>Growth in number of articles:</h4>
 <script src="Chart.js"></script>
 <div class="chart">
 <canvas id="NumberOfArticles" width="400" height="400"></canvas>
 </div>
 <script>
 var ctx = document.getElementById("NumberOfArticles");
 var myChart = new Chart(ctx, {
     type: 'bar',
     data: {
         labels: years,
         datasets: [{
             label: 'size of the AFP in # of articles',
             data: no_articles,
             backgroundColor: "rgba(46, 45, 78, 1)"
         }],
     },
     options: {
         responsive: true,
         maintainAspectRatio: true,
         scales: {
             yAxes: [{
                 ticks: {
                     beginAtZero:true
                 }
             }]
         },
      }
 });
 </script>
 
 <h4>Growth in lines of code:</h4>
 <div class="chart">
 <canvas id="NumberOfLoc" width="400" height="400"></canvas>
 </div>
 <script>
 var ctx = document.getElementById("NumberOfLoc");
 var myChart = new Chart(ctx, {
     type: 'bar',
     data: {
         labels: years,
         datasets: [{
             label: 'size of the AFP in lines of code',
             data: no_loc,
             backgroundColor: "rgba(101, 99, 136, 1)"
         }],
     },
     options: {
         responsive: true,
         maintainAspectRatio: true,
         scales: {
             yAxes: [{
                 ticks: {
                     beginAtZero:true
                 }
             }]
         },
      }
 });
 </script>
 
 <h4>Growth in number of authors:</h4>
 <div class="chart">
 <canvas id="NumberOfAuthors" width="400" height="400"></canvas>
 </div>
 <script>
 var ctx = document.getElementById("NumberOfAuthors");
 var myChart = new Chart(ctx, {
     type: 'bar',
     data: {
         labels: years,
         datasets: [{
             label: 'new authors per year',
             data: no_authors,
             backgroundColor: "rgba(101, 99, 136, 1)"
             },
             {
             label: 'number of authors contributing (cumulative)',
             data: no_authors_series,
             backgroundColor: "rgba(0, 15, 48, 1)"
         }],
     },
     options: {
         responsive: true,
         maintainAspectRatio: true,
         scales: {
             yAxes: [{
                 ticks: {
                     beginAtZero:true
                 }
             }]
         },
      }
 });
 </script>
 
 <h4>Size of articles:</h4>
 <div style="width: 800px" class="chart">
 <canvas id="LocArticles" width="800" height="400"></canvas>
 </div>
 <script>
 var ctx = document.getElementById("LocArticles");
 var myChart = new Chart(ctx, {
     type: 'bar',
     data: {
         labels: years_loc_articles,
         datasets: [{
             label: 'loc per article',
             data: loc_articles,
             backgroundColor: "rgba(101, 99, 136, 1)"
             }]
     },
     options: {
         responsive: true,
         maintainAspectRatio: true,
         scales: {
             xAxes: [{
                 categoryPercentage: 1,
                 barPercentage: 0.9,
                 ticks: {
                     autoSkip: false
                 }
                 }],
             yAxes: [{
                 ticks: {
                     beginAtZero:true
                 }
             }]
         },
         tooltips: {
             callbacks: {
                 title: function(tooltipItem, data) {
                        return all_articles[tooltipItem[0].index];
                        }
             }
         }
      }
 });
 </script>
 
     </td></tr>
 
   </tbody>
 </table>
 
 </div>
 </td>
 
 </tr>
 </tbody>
 </table>
 
 <script src="Chart.js"></script>
 
 </body>
 </html>
\ No newline at end of file
diff --git a/web/submitting.html b/web/submitting.html
--- a/web/submitting.html
+++ b/web/submitting.html
@@ -1,155 +1,155 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
 <meta charset="utf-8">
 <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">
 <link rel="alternate" type="application/rss+xml" title="RSS" href="rss.xml">
  </head>
 
 <body class="mathjax_ignore">
 
 <table width="100%">
 <tbody>
 <tr>
 
 <!-- Navigation -->
 <td width="20%" align="center" valign="top">
   <p>&nbsp;</p>
   <a href="https://www.isa-afp.org/">
     <img src="images/isabelle.png" width="100" height="88" border=0>
   </a>
   <p>&nbsp;</p>
   <p>&nbsp;</p>
   <table class="nav" width="80%">
     <tr>
       <td class="nav" width="100%"><a href="index.html">Home</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="about.html">About</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="submitting.html">Submission</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="updating.html">Updating Entries</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="using.html">Using Entries</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="search.html">Search</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="statistics.html">Statistics</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="topics.html">Index</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="download.html">Download</a></td>
     </tr>
   </table>
   <p>&nbsp;</p>
   <p>&nbsp;</p>
 </td>
 
 
 <!-- Content -->
 <td width="80%" valign="top">
 <div align="center">
   <p>&nbsp;</p>
   <h1><font class="first">S</font>ubmission
 <font class="first">G</font>uidelines
 </h1>
   <p>&nbsp;</p>
 
 <table width="80%" class="descr">
   <tbody>
     <tr><td>
 
 <p>Please send your submission
 <a href="https://ci.isabelle.systems/afp-submission/">via this web page</a>.
 </p>
 
 <p><strong>The submission must follow the following Isabelle style rules.</strong>
     For additional guidelines on Isabelle proofs, also see the this <a href="http://proofcraft.org/blog/isabelle-style.html">guide</a> (feel free to follow all of these; only the below are mandatory).
     <strong>Technical details about the submission process and the format of the submission are explained on the submission site.</strong></p>
 <ul>
     <li>No use of the commands <code>sorry</code> or <code>back</code>.</li>
 
     <li>Instantiations must not use Isabelle-generated names such as
     <code>xa</code> &mdash; use Isar, the <code>subgoal</code> command
     or <code>rename_tac</code> to avoid such names.</li>
 
     <li>No use of the command <code>smt_oracle</code>.</li>
 
     <li>If your theories contain calls to <code>nitpick</code>,
     <code>quickcheck</code>, or <code>nunchaku</code> those calls must
     include the <code>expect</code> parameter. Alternatively the
     <code>expect</code> parameter must be set globally via, e.g.
     <code>nitpick_params</code>.</li>
 
     <li><code>apply</code> scripts should be indented by subgoal as in
     the Isabelle distribution. If an <code>apply</code> command is
     applied to a state with <code>n+1</code> subgoals, it must be
     indented by <code>n</code> spaces relative to the first
     <code>apply</code> in the sequence.</li>
 
     <li>Only named lemmas should carry attributes such as <code>[simp]</code>.</li>
 
     <li>We prefer structured Isar proofs over apply style, but do not
     mandate them.</li>
 
     <li>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.</li>
 
     <li>The entry must contain a ROOT file with one session that has the
         name of the entry. We strongly encourage precisely one session per
         entry, but exceptions can be made. All sessions must be in group
         (AFP), and all theory files of the submission must be contained in
-        at least one session. See also the example <a href="https://bitbucket.org/isa-afp/afp-2018/src/default/thys/Example-Submission/ROOT">ROOT</a> file
+        at least one session. See also the example <a href="https://foss.heptapod.net/isa-afp/afp-2020/-/blob/branch/default/thys/Example-Submission/ROOT">ROOT</a> file
         in the <a href="entries/Example-Submission.html">Example submission</a>.
 	</li>
 
     <li>The entry should cite all sources that the theories are based on,
     for example textbooks or research articles containing informal versions of the proofs.</li>
 </ul>
 
 <p>Your submission must contain an abstract to be displayed on the web site &ndash; usually this will be the same as the abstract of your proof document in the <tt>root.tex</tt> file. You can use LaTeX formulae in this web site abstract, either inline formulae in the form <tt>$a+b$</tt> or <tt>\(a+b\)</tt> or display formulae in the form <tt>$$a + b$$</tt> or <tt>\[a + b\]</tt>. Other occurrences of these characters must be escaped (e.g. <tt>\$</tt> or <tt>\\(</tt>). Note that LaTeX in the title of an entry is <em>not</em> allowed. Most basic LaTeX functionality should be supported. For details on what parts of LaTeX are supported, see the <a href="https://docs.mathjax.org/en/v2.7-latest/tex.html">MathJax documentation.</a></p>
 
 <p>It is possible and encouraged to build on other archive entries
    in your submission. There is a standardised way to
    <a href="using.html">refer to other AFP entries</a> in your
    theories.</p>
 
 <p>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.</p>
 
 <p>If you have questions regarding your submission, please email <a
 href="&#109;&#97;&#105;&#108;&#116;&#111;:&#97;&#102;&#112;-&#115;&#117;&#98;&#109;&#105;&#116;&#64;&#105;&#110;&#46;&#116;&#117;&#109;&#46;&#100;&#101;">&#97;&#102;&#112;-&#115;&#117;&#98;&#109;&#105;&#116;&#64;&#105;&#110;&#46;&#116;&#117;&#109;&#46;&#100;&#101;</a>.
       If you need help with Isabelle, please use the
 <a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
       mailing list. It is always a good idea to <a
       href="https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users">subscribe</a>.</p>
 
     </td></tr>
   </tbody>
 </table>
 
 
 </div>
 </td>
 
 </tr>
 </tbody>
 </table>
 
 
 </body>
 </html>
\ No newline at end of file
diff --git a/web/updating.html b/web/updating.html
--- a/web/updating.html
+++ b/web/updating.html
@@ -1,170 +1,170 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
 <meta charset="utf-8">
 <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">
 <link rel="alternate" type="application/rss+xml" title="RSS" href="rss.xml">
  </head>
 
 <body class="mathjax_ignore">
 
 <table width="100%">
 <tbody>
 <tr>
 
 <!-- Navigation -->
 <td width="20%" align="center" valign="top">
   <p>&nbsp;</p>
   <a href="https://www.isa-afp.org/">
     <img src="images/isabelle.png" width="100" height="88" border=0>
   </a>
   <p>&nbsp;</p>
   <p>&nbsp;</p>
   <table class="nav" width="80%">
     <tr>
       <td class="nav" width="100%"><a href="index.html">Home</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="about.html">About</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="submitting.html">Submission</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="updating.html">Updating Entries</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="using.html">Using Entries</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="search.html">Search</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="statistics.html">Statistics</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="topics.html">Index</a></td>
     </tr>
     <tr>
       <td class="nav"><a href="download.html">Download</a></td>
     </tr>
   </table>
   <p>&nbsp;</p>
   <p>&nbsp;</p>
 </td>
 
 
 <!-- Content -->
 <td width="80%" valign="top">
 <div align="center">
   <p>&nbsp;</p>
   <h1><font class="first">U</font>pdating
 <font class="first">E</font>ntries
 </h1>
   <p>&nbsp;</p>
 
 <table width="80%" class="descr">
   <tbody>
     <tr><td>
 
 <h2>Change</h2>
 <p>
 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
 authors.
 </p>
 <p>
 This conflicts with the purpose of archiving and preserving
-entries as they have been submitted and with the purpose of 
+entries as they have been submitted and with the purpose of
 providing a clear and simple interface to readers.
 </p>
 <p>
 The AFP deals with this by synchronizing such updates with
 Isabelle releases:
 </p>
 <ul>
 <li>
 The entries released and visible on the main site are always
 working with the most recent stable Isabelle version and do not
 change.
 </li>
 <li>
 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 <a
-href="https://bitbucket.org/isa-afp/afp-devel/">bitbucket
+href="https://foss.heptapod.net/isa-afp/afp-devel/">Heptapod
 mercurial repository</a> or as tar.gz package on the <a href="download.html">
 download page</a>.
 </li>
 <li>
 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
 accessible.
 </li>
 </ul>
 
 <p>
 Significant changes of an entry should be recorded in the metadata of the
 entry using the keyword "extra-history". The resulting web page should look
 <a href="https://www.isa-afp.org/entries/JinjaThreads.html">something like this</a>.
 </p>
 
 <h2>Monotonicity</h2>
 
 <p>
 Updating an entry should be mostly monotone: you add new material, but you do
 not modify existing material in a major way. Ideally, entries (by other
 people) that build on yours should not be affected. Otherwise you have to
 liaise with them first. If you intend to carry out major non-monotone
 changes, you will need to submit a completely new entry (with a description
 of how it relates to the old one). This should be required only very rarely:
 AFP entries should be mature enough not to require major changes to their
 interface (i.e. the main functions and theorems provided).
 </p>
 
 <p>
 Major monotone changes, e.g. adding a new concept rather than more results on
 existing concepts, may also call for a new entry, but one that builds on the
 existing one. This depends on how you would like to organize your entries.
 </p>
 
 <h2>If you are an author</h2>
 
 <p>
 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.
 </p>
 <p>
 To achieve this, you should base your changes on the <a
-href="https://bitbucket.org/isa-afp/afp-devel/">mercurial 
+href="https:/foss.heptapod.net/isa-afp/afp-devel/">mercurial
 development version</a>
 of your AFP entry and test it against the current <a
 href="http://isabelle.in.tum.de/devel/">Isabelle development
 version</a>.
 </p>
 <p>
-If you would like to get write access to your entry in the 
+If you would like to get write access to your entry in the
 mercurial repository or if you need
 assistance, please contact the <a href="about.html#editors">editors</a>.
 </p>
 
     </td></tr>
   </tbody>
 </table>
 
 </div>
 </td>
 
 </tr>
 </tbody>
 </table>
 
 
 </body>
 </html>
\ No newline at end of file