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,600</td></tr>
 <tr><td>Lines of Code:</td><td class="statsnumber">~2,568,200</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, 238900.0, 353800.0, 435900.0, 517100.0, 568100.0, 740400.0, 828100.0, 1038200.0, 1216500.0, 1580000.0, 1829400.0, 2101100.0, 2395300.0, 2568200.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","17203","3119","6430","1145","447","2537","1275","1583","1838","12833","13114","2685","1228","3556","4269","9649","970","2847","1741","79734","4738","3396","2186","31192","10664","6723","30332","180","794","1047","14411","2080","254","2221","5958","3462","799","1540","684","6654","8","2627","27490","330","32412","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","1620","16","2930","7805","6557","6381","992","125","10136","332","235","1828","1039","1784","4425","303","4461","11857","2834","8583","1043","408","2940","2613","38065","3243","1480","2611","3153","27588","2580","25275","2266","4107","7701","1245","260","5309","73","9729","719","6673","1511","4354","1248","1908","6215","4974","10067","7894","538","3830","4595","202","848","1781","5209","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","5930","1829","12832","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","8635","3142","9161","690","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","3813","656","329","1057","8313","3257","2593","553","8478","206","17950","8773","3315","398","2960","12833","9483","373","173","384","18976","2545","6119","3777","1017","1889","4338","9356","20034","4053","3420","319","3204","169","19540","541","14618","2648","7033","7590","3898","3244","4507","855","2289","5004","1349","276","4339","1475","3482","7115","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","7461","5301","3079","2808","8849","5261","2328","5861","945","6519","992","489","809","8891","3133","338","854","493","4585","9457","15962","6058","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","10027","2667","541","1271","3955","5318","9770","2765","934","11924","1743","2355","7917","1490","449","685","1811","1132","3248","3578","1644","2983","2218","7221","4968","2767","15247","34365","3259","6022","1900","372","10334","16867","3018","3300","5302","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","6605","4830","5723","4561","10314","14529","6402","4407","1907","51409","2450","3948","2758","1699","3154","944","906","596","375","691","766","2564","332","14517","21769","11343","3391","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","17203","3119","6430","1145","447","2537","1275","1583","1838","12833","13114","2685","1228","3556","4269","9649","970","2847","1741","79734","4738","3396","2186","31192","10664","6723","30332","180","794","1047","14411","2080","254","2221","5958","3462","799","1540","684","6654","8","2627","27490","330","32412","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","1620","16","2930","7805","6557","6381","992","125","10136","332","235","1828","1039","1784","4425","303","4461","11857","2834","8583","1043","408","2940","2613","38065","3243","1480","2611","3153","27588","2580","25275","2266","4107","7701","1245","260","5309","73","9729","719","6673","1511","4354","1248","1908","6215","4974","10067","7894","538","3830","4595","202","848","1781","5209","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","5930","1829","12832","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","8635","3142","9161","690","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","3813","656","329","1057","8313","3257","2593","553","8478","206","17950","8773","3315","398","2960","12833","9483","373","173","384","18976","2545","6119","3777","1017","1889","4338","9356","20034","4053","3420","319","3204","169","19540","541","14618","2648","7033","7590","3898","3244","4507","855","2289","5004","1349","276","4339","1475","3482","7115","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","7461","5301","3079","2808","8849","5261","2328","5861","945","6519","992","489","809","8891","3133","338","854","493","4585","9457","15962","6058","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","10025","2667","541","1271","3955","5318","9770","2765","934","11924","1743","2355","7917","1490","449","685","1811","1132","3248","3578","1644","2983","2218","7221","4968","2767","15247","34365","3259","6022","1900","372","10334","16867","3018","3300","5302","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","6605","4830","5723","4561","10314","14529","6402","4407","1907","51409","2450","3948","2758","1699","3154","944","906","596","375","691","766","2564","332","14517","21769","11343","3391","744","2351","1559","1239","1609","2537","1939","1341","12003","1034","1444","1938","2670","827","12969","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