diff --git a/admin/site/content/about.md b/admin/site/content/about.md
--- a/admin/site/content/about.md
+++ b/admin/site/content/about.md
@@ -1,54 +1,54 @@
 ---
 title: "About"
 menu: 
     main:
         name: "About"
         weight: 6
 ---
 
 The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments,
 mechanically checked in the theorem prover Isabelle.
 It is organized in the way of a scientific journal.
 [Submissions](/submission) are refereed.
 
 The archive repository is hosted on [Heptapod](https://foss.heptapod.net/isa-afp/) 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.
 
 ## Editors
 
 The editors of the Archive of Formal Proofs are:
 
-*   [Manuel Eberl](http://www.in.tum.de/~eberlm/), [Technische Universität München](http://www.tum.de/)
-*   [Gerwin Klein](http://www.cse.unsw.edu.au/~kleing/), [Data61](http://www.data61.csiro.au)
-*   [Tobias Nipkow](http://www.in.tum.de/~nipkow/), [Technische Universität München](http://www.tum.de/)
-*   [Larry Paulson](http://www.cl.cam.ac.uk/users/lcp/), [University of Cambridge](http://www.cam.ac.uk/)
+*   [Manuel Eberl](https://www.in.tum.de/~eberlm/), [Technische Universität München](https://www.tum.de/)
+*   [Gerwin Klein](https://www.cse.unsw.edu.au/~kleing/), [Data61](https://www.data61.csiro.au)
+*   [Tobias Nipkow](https://www.in.tum.de/~nipkow/), [Technische Universität München](https://www.tum.de/)
+*   [Larry Paulson](https://www.cl.cam.ac.uk/users/lcp/), [University of Cambridge](https://www.cam.ac.uk/)
 *   [René Thiemann](http://cl-informatik.uibk.ac.at/users/thiemann/), [University of Innsbruck](https://www.uibk.ac.at/)
 
 ## Why
 
 We aim to strengthen the community and to foster the development of formal proofs.
 
 We hope that the Archive will provide:
 
 *   a resource of knowledge, examples, and libraries for users,
 *   a large and relevant test bed of theories for Isabelle developers, and
 *   a central, citable place for authors to publish their theories
 
 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.
 
 ## License
 
-All entries in the Archive of Formal Proofs are licensed under a [BSD-style License](LICENSE) or the [GNU LGPL](http://www.gnu.org/copyleft/lesser.html). This means they are free to download, free to use, free to change, and free to redistribute with minimal restrictions.
+All entries in the Archive of Formal Proofs are licensed under a [BSD-style License](LICENSE) or the [GNU LGPL](https://www.gnu.org/copyleft/lesser.html). This means they are free to download, free to use, free to change, and free to redistribute with minimal restrictions.
 
 The authors retain their full copyright on their original work, including their right to make the development available under another, additional license in the future.
 
 ## Website
 
 This website is the result of a project from the School of Informatics at the [University of Edinburgh](https://www.ed.ac.uk) by:
  * Carlin MacKenzie, [AIML](https://aiml.inf.ed.ac.uk)
- * James Vaughan, [AIAI](http://web.inf.ed.ac.uk/aiai/)
- * Jacques Fleuriot, [AIAI](http://web.inf.ed.ac.uk/aiai/)
+ * James Vaughan, [AIAI](https://web.inf.ed.ac.uk/aiai/)
+ * Jacques Fleuriot, [AIAI](https://web.inf.ed.ac.uk/aiai/)
 
 Integration and maintenance by:
- * [Fabian Huch](https://www21.in.tum.de/team/huch), [Technische Universität München](http://www.tum.de/)
+ * [Fabian Huch](https://www21.in.tum.de/team/huch), [Technische Universität München](https://www.tum.de/)
diff --git a/admin/site/content/download.md b/admin/site/content/download.md
--- a/admin/site/content/download.md
+++ b/admin/site/content/download.md
@@ -1,31 +1,31 @@
 ---
 title: Download the Archive
 menu: 
     main:
         name: "Download"
         weight: 3
 ---
 
 ### **Current stable version** (for most recent Isabelle release):
 
 Download all sessions: {{< download href="https://www.isa-afp.org/release/afp-current.tar.gz" label="afp-current.tar.gz (~70 MB)" >}}
 
 ### Older stable versions:
 
-Please use the [sourceforge download system](http://sourceforge.net/projects/afp/files/) to access older versions of the archive.
+Please use the [sourceforge download system](https://sourceforge.net/projects/afp/files/) to access older versions of the archive.
 
 ### Mercurial access:
 
 At [Heptapod](https://foss.heptapod.net/isa-afp/afp-devel/) (development version of the Archive, for the development version of Isabelle)
 
 ### Metadata download
 
 The metadata of all entries is available as an array of JSON objects: {{< download href="/release/metadata.json" label="metadata.json (~1 MB)" >}}
 
 ### How to refer to AFP entries:
 
 You can refer to AFP entries by using the [AFP as an Isabelle component](/help).
 
 The AFP repository is hosted on [Heptapod](https://foss.heptapod.net/), a friendly fork of GitLab for Mercurial provided by [Octobus](https://octobus.net) and [Clever Cloud](https://www.clever-cloud.com/en/).
 
 ![Octobus and Clever Cloud logos](/images/octobus+clever.png)
diff --git a/admin/site/content/help.md b/admin/site/content/help.md
--- a/admin/site/content/help.md
+++ b/admin/site/content/help.md
@@ -1,62 +1,62 @@
 ---
 title: Help
 menu: 
     main:
         name: "Help"
         weight: 4
 ---
 
 This section focuses on the Archive of Formal Proofs. For help with Isabelle, see the [Isabelle Wiki](https://isabelle.in.tum.de/community/Main_Page) and [Documentation](https://isabelle.in.tum.de/documentation.html)
 
 ## Referring to AFP Entries in Isabelle/JEdit
 
 Once you have downloaded the AFP, you can include its articles and theories in your own developments. If you would like to make your work available to others _without_ having to include the AFP articles you depend on, here is how to do it.
 
 From Isabelle2021 on, the recommended method for making the whole AFP available to Isabelle is the `isabelle components -u` command.
 
 #### Linux and Mac
 
 Assuming you have downloaded and unzipped the afp to `/home/myself/afp`, run:
 
     isabelle components -u /home/myself/afp
 
 #### Windows
 
 If the AFP is in `C:\afp`, run the following command in a Cygwin terminal:
 
     isabelle components -u /cygdrive/c/afp
 
 #### Use
 
 You can now refer to article `ABC` from the AFP in another theory via:
 
     imports "ABC.Some_ABC_Theory"
 
 This allows you to distribute your material separately from any AFP theories. Users of your distribution also need to install the AFP in the above manner.
 
 
 ## Citing Entries
 
 The following gives an example of the preferred way for citing entries in the AFP:
 
-> M. Jaskelioff and S. Merz, Proving the Correctness of Disk Paxos. _Archive of Formal Proofs_, June 2005, [http://isa-afp.org/entries/DiskPaxos.html](http://isa-afp.org/entries/DiskPaxos.html), Formal proof development.
+> M. Jaskelioff and S. Merz, Proving the Correctness of Disk Paxos. _Archive of Formal Proofs_, June 2005, [https://isa-afp.org/entries/DiskPaxos.html](https://isa-afp.org/entries/DiskPaxos.html), Formal proof development.
 
 The bibtext entry for this would be:
 
 ```
 @article{Jaskelioff-Merz-AFP05,
   author =   {Mauro Jaskelioff and Stephan Merz},
   title =    {Proving the Correctness of Disk Paxos},
   journal =  {Archive of Formal Proofs},
   month =    Jun,
   year =     2005,
-  note =     {\\url{http://isa-afp.org/entries/DiskPaxos.html}, Formal proof development},
+  note =     {\\url{https://isa-afp.org/entries/DiskPaxos.html}, Formal proof development},
   ISSN =     {2150-914x}
 }
 ```
 
 ## Mailing Lists
 
 * isabelle-users@cl.cam.ac.uk provides a forum for Isabelle users to discuss problems, exchange information, and make announcements. Users of official Isabelle releases should subscribe or see the archive.
     
 * isabelle-dev@in.tum.de covers the Isabelle development process, including intermediate repository versions, and administrative issues concerning the website or testing infrastructure. Early adopters of development snapshots or repository versions should subscribe or see the archive (also available at mail-archive.com).
diff --git a/admin/site/content/submission.md b/admin/site/content/submission.md
--- a/admin/site/content/submission.md
+++ b/admin/site/content/submission.md
@@ -1,63 +1,63 @@
 ---
 title: Entry Submission
 menu: 
     bottom:
         name: "Submission"
 ---
 
 ## Submission Guidelines
 
-**The submission must follow the following Isabelle style rules.** For additional guidelines on Isabelle proofs, also see the this [guide](http://proofcraft.org/blog/isabelle-style.html) (feel free to follow all of these; only the below are mandatory). **Technical details about the submission process and the format of the submission are explained on the submission site.**
+**The submission must follow the following Isabelle style rules.** For additional guidelines on Isabelle proofs, also see the this [guide](https://proofcraft.org/blog/isabelle-style.html) (feel free to follow all of these; only the below are mandatory). **Technical details about the submission process and the format of the submission are explained on the submission site.**
 
 *   No use of the commands `sorry` or `back`.
 *   Instantiations must not use Isabelle-generated names such as `xa` — use Isar, the `subgoal` command or `rename_tac` to avoid such names.
 *   No use of the command `smt_oracle`.
 *   If your theories contain calls to `nitpick`, `quickcheck`, or `nunchaku` those calls must include the `expect` parameter. Alternatively the `expect` parameter must be set globally via, e.g. `nitpick_params`.
 *   `apply` scripts should be indented by subgoal as in the Isabelle distribution. If an `apply` command is applied to a state with `n+1` subgoals, it must be indented by `n` spaces relative to the first `apply` in the sequence.
 *   Only named lemmas should carry attributes such as `[simp]`.
 *   We prefer structured Isar proofs over apply style, but do not mandate them.
 *   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.
 *   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 [ROOT](https://foss.heptapod.net/isa-afp/afp-2020/-/blob/branch/default/thys/Example-Submission/ROOT) file in the [Example submission](/entries/Example-Submission.html).
 *   The entry should cite all sources that the theories are based on, for example textbooks or research articles containing informal versions of the proofs.
 
 Your submission must contain an abstract to be displayed on the web site – usually this will be the same as the abstract of your proof document in the root.tex file. You can use LaTeX formulae in this web site abstract, either inline formulae in the form $a+b$ or \\(a+b\\) or display formulae in the form $$a + b$$ or \\\[a + b\\\]. Other occurrences of these characters must be escaped (e.g. \\$ or \\\\(). Note that LaTeX in the title of an entry is _not_ allowed. Most basic LaTeX functionality should be supported. For details on what parts of LaTeX are supported, see the [MathJax documentation.](https://docs.mathjax.org/en/v2.7-latest/tex.html)
 
 It is possible and encouraged to build on other archive entries in your submission. There is a standardised way to [refer to other AFP entries](/help) in your theories.
 
 ## Submission Form
 
 Please send your submission [via this web page](https://ci.isabelle.systems/afp-submission/).
 
 Your submission will be refereed and you will receive notification as soon as possible. If accepted, you must agree to maintain your archive entry or nominate someone else to maintain it. The Isabelle development team will assist with maintenance, but it does not have the resources to fully maintain the complete archive.
 
 If you have questions regarding your submission, please email [afp-submit@in.tum.de](mailto:afp-submit@in.tum.de). If you need help with Isabelle, please use the [isabelle-users@cl.cam.ac.uk](mailto:isabelle-users@cl.cam.ac.uk) mailing list. It is always a good idea to [subscribe](https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users).
 
 # Updating Entries
 
 ## Change
 
 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.
 
 This conflicts with the purpose of archiving and preserving entries as they have been submitted and with the purpose of providing a clear and simple interface to readers.
 
 The AFP deals with this by synchronizing such updates with Isabelle releases:
 
 *   The entries released and visible on the main site are always working with the most recent stable Isabelle version and do not change.
 *   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 [Heptapod mercurial repository](https://foss.heptapod.net/isa-afp/afp-devel/) or as tar.gz package on the [download page](/download).
 *   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.
 
 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 [something like this](https://www.isa-afp.org/entries/JinjaThreads.html).
 
 ## Monotonicity
 
 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).
 
 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.
 
 ## If you are an author
 
 The above means that if you are an author and would like to provide a new, better version of your AFP entry, you can do so.
 
-To achieve this, you should base your changes on the [mercurial development version](https:/foss.heptapod.net/isa-afp/afp-devel/) of your AFP entry and test it against the current [Isabelle development version](http://isabelle.in.tum.de/devel/).
+To achieve this, you should base your changes on the [mercurial development version](https:/foss.heptapod.net/isa-afp/afp-devel/) of your AFP entry and test it against the current [Isabelle development version](https://isabelle.in.tum.de/devel/).
 
 If you would like to get write access to your entry in the mercurial repository or if you need assistance, please contact the [editors](/about#editors).
diff --git a/admin/site/themes/afp/layouts/entries/single.html b/admin/site/themes/afp/layouts/entries/single.html
--- a/admin/site/themes/afp/layouts/entries/single.html
+++ b/admin/site/themes/afp/layouts/entries/single.html
@@ -1,155 +1,155 @@
 {{- define "main" -}}
 {{- $site := . -}}
 {{- $path := .Site.Params.afpUrls.html -}}
 {{- if isset .Site.Data "status" -}}
   {{- $path = .Site.Params.afpUrls.htmlDevel -}}
 {{- end -}}
 {{- $entry_name := .File.BaseFileName -}}
 <main>
   {{- if isset .Site.Data "status" -}}
   <strong>
     This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.
   </strong>
   {{- end -}}
   <h3>Abstract</h3>
 
   <div class="abstract mathjax_process">{{- trim .Params.abstract "\n" | safeHTML -}}</div>
   {{- if (eq .Params.licence "BSD") -}}
-  <a href="http://isa-afp.org/LICENSE">BSD License</a>
+  <a href="https://isa-afp.org/LICENSE">BSD License</a>
   {{- else if (eq .Params.license "LGPL") -}}
-  <a href="http://isa-afp.org/LICENSE.LGPL">GNU Lesser General Public License (LGPL)</a>
+  <a href="https://isa-afp.org/LICENSE.LGPL">GNU Lesser General Public License (LGPL)</a>
   {{- else -}}
     {{- printf "%s License" .Params.license -}}
   {{- end -}}
 
   {{- with .Params.extra -}}
   {{- range $key, $value := . -}}
   <h3>{{- humanize $key -}}</h3>
 
   <p>{{- $value | safeHTML -}}</p>
   {{- end -}}
   {{- end -}}
 
   {{- $Scratch := newScratch -}}
   
   {{- with .Params.dependencies -}}
     <h3>Depends On</h3><ul>
       {{- range . -}}
       <li>{{- printf "[%s](/entries/%s.html)" . . | $.Page.RenderString -}}</li>
       {{- end -}}
     </ul>
   {{- end -}}
 
   {{- with (index .Site.Taxonomies.dependencies (urlize $entry_name)) -}}
     <h3>Used by</h3>
     <ul>
       {{- range . -}}
       <li>{{- printf "[%s](%s)" .File.BaseFileName .RelPermalink | $.Page.RenderString -}}</li>
       {{- end -}}
     </ul>
   {{- end -}}
 
   {{- with .Params.topics -}}
   <h3>Topics</h3>
   <ul>
     {{- range . -}}
     <li>{{- printf "[%s](/topics/%s)" . (urlize .) | $.Page.RenderString -}}</li>
     {{- end -}}
   </ul>
   {{- end -}}
 
 
   {{- range .Params.sessions -}}
   {{ $session := .session }}
   <h3>Theories of {{ $session }}</h3>
   <ul>
     {{- range .theories }}
     <li><a href="/theories/{{ urlize $session }}/#{{ . }}">{{ . }}</a></li>
     {{- end -}}
   </ul>
   {{- end -}}
 
   {{ $related := .Site.RegularPages.Related . | first 3 }}
   {{ with $related }}
   <h3>Related Entries</h3>
   <ul>
     {{ range . }}
     <li>{{- printf "[%s](%s)" .Title .RelPermalink | $.Page.RenderString -}}</li>
     {{ end }}
   </ul>
   {{ end }}
 </main>
 
 {{- if isset .Site.Data "status" -}}
   <nav>
   {{- $status := "none" -}}
   {{- range where .Site.Data.status.entries "entry" $entry_name -}}
     {{- $status = .status -}}
   {{- end -}}
     <div class="status-{{ $status }}">
       <p>Status: <strong>{{- $status -}}</strong></p>
       <p>{{ .Site.Data.status.build_data.time }}</p>
       <p>Isabelle/<wbr>{{ .Site.Data.status.build_data.isabelle_id }}</p>
       <p>AFP/<wbr>{{ .Site.Data.status.build_data.afp_id }}</p>
       <p><a href="{{ .Site.Data.status.build_data.url }}">{{ .Site.Data.status.build_data.job }}</a></p>
     </div>
   </nav>
 {{- else -}}
 <nav class='links'>
   <a class='popup-button' href="#citePopUp">Cite</a>
   <a class='popup-button' href="#download-popup">Download</a>
   <h4>PDFs</h4>
   <a href="{{- $path -}}/{{- $entry_name -}}/outline.pdf">Proof
     outline</a>
   <a href="{{- $path -}}/{{- $entry_name -}}/document.pdf">Proof
     document</a>
   <a href="{{- $path -}}/{{- $entry_name -}}/session_graph.pdf">Dependencies</a>
 </nav>
 
 <div id="citePopUp" class="overlay">
   <a class="cancel" href="#"></a>
   <div class="popup">
     <h2>Cite</h2>
     <a class="close" href="#">&times;</a>
     <div>
       <p style="display:none;" id="bibtexFileName">{{- $entry_name -}}-AFP</p>
       <pre id="copyText">@article{{- "{" -}}{{- $entry_name -}}-AFP,
   author  = {{ "{" -}}{{- delimit .Params.authors ", " | replaceRE "(, )([^,]+$)" " and $2" -}}},
   title   = {{ "{" -}}{{- htmlUnescape .Params.title -}}},
   journal = {Archive of Formal Proofs},
   month   = {{ dateFormat "January" .Params.date -}},
   year    = {{ dateFormat "2006" .Params.date -}},
-  note    = {\url{http://isa-afp.org/entries/{{- $entry_name -}}.html},
+  note    = {\url{https://isa-afp.org/entries/{{- $entry_name -}}.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }</pre>
       <button id="copyBibtex">Copy</button> <a id="downloadBibtex">Download</a>
     </div>
   </div>
 </div>
 
 <div id="download-popup" class="overlay">
   <a class="cancel" href="#"></a>
   <div class="popup">
     <h2>Download</h2>
     <a class="close" href="#">&times;</a>
     <a href="https://isa-afp.org/release/afp-{{- $entry_name -}}-current.tar.gz" download>Download latest</a>
     {{ with .Params.olderReleases -}}
     <p>Older releases:</p>
     <ul>
       {{- range $map := . -}}
       {{- range $key, $value := $map -}}
       <li>Isabelle {{- $key -}}:
         <a href="https://isa-afp.org/release/afp-{{- $entry_name -}}-{{- $value -}}.tar.gz">
           afp-{{- $entry_name -}}-{{- $value -}}.tar.gz
         </a>
       </li>
       {{- end -}}
       {{- end -}}
     </ul>
     {{- end }}
   </div>
 </div>
 {{- end -}}
 
 {{- end -}}
diff --git a/admin/site/themes/afp/layouts/index.html b/admin/site/themes/afp/layouts/index.html
--- a/admin/site/themes/afp/layouts/index.html
+++ b/admin/site/themes/afp/layouts/index.html
@@ -1,48 +1,50 @@
 {{- define "main" -}}
 <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, is indexed by <a href="http://dblp.uni-trier.de/db/journals/afp/">dblp</a> and has an
-  ISSN:
-  2150-914x. Submissions are refereed and we encourage companion AFP submissions to conference and journal
-  publications. To cite an entry, please use the <a href="/help/#citing-entries">preferred citation style</a>.
+  The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments,
+  mechanically checked in the theorem prover <a href="https://isabelle.in.tum.de/">Isabelle</a>.
+  It is organized in the way of a scientific journal,
+  is indexed by <a href="https://dblp.uni-trier.de/db/journals/afp/">dblp</a>
+  and has an ISSN: 2150-914x.
+  Submissions are refereed and we encourage companion AFP submissions to conference and journal publications.
+  To cite an entry, please use the <a href="/help/#citing-entries">preferred citation style</a>.
+</p>
+<p>
+  A <a href="https://devel.isa-afp.org/">development version</a> of the archive is available as well.
 </p>
 
 {{- if isset .Site.Data "status" -}}
 <p>
 <strong>
 This is the development version of the archive, referring to a recent Isabelle development version.
 Some entries may not be in a working state.
-The main archive is available from the <a href="http://www.isa-afp.org/">front page</a>.
+The main archive is available from the <a href="https://www.isa-afp.org/">front page</a>.
 </strong>
 </p>
 {{- end -}}
 
 <form autocomplete="off" action="{{ "search" | absURL }}">
   <div class='form-container'>
     <input id="search-input" type="search" size="31" maxlength="255" value="" aria-label="Search the AFP" list="autocomplete"><button
       id="search-button" type="button">Search</button>
     <datalist id="autocomplete">
     </datalist>
   </div>
 </form>
 
 {{- range (where site.RegularPages "Type" "in" site.Params.mainSections).GroupByDate "2006" -}}
 <div>
   <h2 class="year">{{- .Key -}}</h2>
   {{- range .Pages }}
   <article class="entry">
     <div class="item-text">
       <h5><a class="title" href="{{ .RelPermalink }}">{{- htmlUnescape .Title -}}</a></h5> <br>
         by {{ partial "authors.html" (dict "site" . "authors" .Params.authors) -}}
     </div>
     <span class="date">
       {{ .Date.Format "Jan 02" }}
     </span>
   </article>
   {{- end -}}
 </div>
 {{- end -}}
 {{- end -}}
\ No newline at end of file
diff --git a/admin/site/themes/afp/layouts/shortcodes/submission.html b/admin/site/themes/afp/layouts/shortcodes/submission.html
--- a/admin/site/themes/afp/layouts/shortcodes/submission.html
+++ b/admin/site/themes/afp/layouts/shortcodes/submission.html
@@ -1,393 +1,393 @@
 <div id="rightbox">
   <table class="entries">
     <tbody>
       <tr>
         <td>
 
           <a href="top"></a>
           <h2 id="hide-toggle" class="hide-button">Submission Guidelines</h2>
           <div id="hide">
             <p class="example"><a href="#form">(Jump to submission form)</a></p>
 
             <p>The submission must build with the current Isabelle release version.
               Submissions for older Isabelle versions are not accepted.</p>
 
             <p>Submissions for the Isabelle development version are also acceptable,
               but publication of the entry on the front page will be deferred until the
               next Isabelle release. In the meantime the entry will only be visible on
               the <a href="https://devel.isa-afp.org">development pages</a>.
               In this case,
               submit your article as described above. Because your article is tested
               against the release version, this will fail (otherwise your article does
               not need the development version!) and you cannot perform the final step
               in the submission process. When that happens, simply copy the url of the
               submission page at that point into an email to <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>.
             </p>
 
             <p>To submit your contribution, you need to create a zip or tar archive containing all your
               theories, including a ROOT file. All files need to reside in a folder that has the same name
               as the short article name (see below). When submitting multiple entries at once, there must be
               one entry per folder and one ROOT file per entry. If you don't already have a ROOT file, refer
-              to the <a href="http://isabelle.in.tum.de/doc/system.pdf">system manual</a> for how to create
+              to the <a href="https://isabelle.in.tum.de/doc/system.pdf">system manual</a> for how to create
               one.</p>
 
             <p>There is also a self-contained
               <a href="https://www.isa-afp.org/entries/Example-Submission.shtml">example submission</a>
               that contains further information, including the structure of the entry and its ROOT file.</p>
 
             <p class="example"><a href="#top" class="hide-button">Hide guidelines</a></p>
           </div>
         </td>
       </tr>
     </tbody>
   </table>
 
   <form action="index" method="POST" enctype="multipart/form-data">
     <a name="form"></a>
 
 
     <p>&nbsp;</p>
     <table class="entries">
       <tbody>
         <tr>
           <td>
             <h2>Metadata</h2>
             <input type="hidden" name="numtable" value="0">
             <table class="formtable" id="formtable_0">
               <tr>
                 <td>Title of article:</td>
                 <td><input name="title_0" type="text" value="">
                   <br>
                   <span class="example">Example: <em>Example Submission</em></span>
                 </td>
               </tr>
               <tr>
                 <td>Short article name (folder name):</td>
                 <td><input name="shortname_0" type="text" value="">
                   <br>
                   <span class="example">Example: <em>Example_Submission</em> (name of the folder where
                     your ROOT and theory files reside)
                   </span>
                 </td>
               </tr>
               <tr>
                 <td>Authors:</td>
                 <td><input name="author_0" type="text" value="">
                   <br>
                   <span class="example">
                     Example:
                     <em>
-                      Gerwin Klein &lt;http://www.cse.unsw.edu.au/~kleing/&gt;,
+                      Gerwin Klein &lt;https://www.cse.unsw.edu.au/~kleing/&gt;,
                       Johannes H&ouml;lzl &lt;mailto:hoelzl@in.tum.de&gt;
                     </em>
                   </span>
                 </td>
               </tr>
               <tr>
                 <td>Topics:</td>
                 <td><input name="topic_0" type="text" value="">
                   <br>
                   <span class="example">
                     Example: <em>Computer Science/Security,
                       Computer Science/Programming Languages/Type Systems</em><br>
                     (<a href=https://www.isa-afp.org/topics.shtml>Index of topics</a>)
                   </span>
                 </td>
               </tr>
               <tr>
                 <td>License:</td>
                 <td><label><input type="radio" name="license_0" value="BSD" checked>BSD</label>
                   <label><input type="radio" name="license_0" value="LGPL">LGPL</label>
                   <br>
                   <span class="example">
                     Note: For LGPL submissions, please include the header "License: LGPL" in each file
                   </span>
                 </td>
               </tr>
               <tr>
                 <td>Abstract:</td>
                 <td><textarea name="abstract_0"></textarea>
                   <br>
                   <span class="example">
                     Note: You can use HTML to format your abstract.
                   </span>
                 </td>
               </tr>
             </table>
             <p>
               <a href="javaScript:void(0);" class="removeField">Remove this entry</a>
             </p>
           </td>
         </tr>
       </tbody>
     </table>
 
     <p>&nbsp;</p>
 
     <table class="entries">
       <tbody>
         <tr>
           <td>
             <p>
               You can submit multiple entries at once. Put the corresponding folders in
               the archive and use the button below to add more input fields for metadata.
             </p>
             <a href="javaScript:void(0);" id="newFields">Add new entry</a><br>
           </td>
         </tr>
       </tbody>
     </table>
 
     <p>&nbsp;</p>
 
     <table class="entries">
       <tbody>
         <tr>
           <td>
             <table id="formtable_end">
               <tr>
                 <td>
                   Contact:
                 </td>
                 <td>
                   <input name="contact" type="text" value="">
                   <br>
                   <span class="example">
                     Example:
                     <em>hoelzl@in.tum.de, haslbecm@in.tum.de</em>
                     (These addresses serve two purposes: 1. They are used to send you updates about
                     the state of your submission. 2. They are the maintainers of the entry once it
                     is accepted. Typically this will be one or more of the authors. You can supply
                     multiple addresses seperated by commas.)
                   </span>
                 </td>
               </tr>
               <tr>
                 <td>
                   Message for the editors:<br>
                 </td>
                 <td>
                   <textarea name="comment"></textarea>
                   <br>
                   <span class="example">
                     Note:
                     Anything special or noteworthy about your submission can be covered here.
                     It will not become part of your entry. You're also welcome to leave
                     suggestions for our AFP submission service here. (Can be left empty)
                   </span>
                 </td>
               </tr>
               <tr>
                 <td>
                   Archive file (.tar.gz or .zip):
                 </td>
                 <td>
                   <input name="tar" type="file">
                   <br>
                   <span class="example">
                     Note: Your zip or tar file should contain one folder with your theories, ROOT,
                     etc. The folder name should be the short/folder name used in the
                     submission form.
                   </span>
                 </td>
               </tr>
               <tr>
                 <td>
                   <input name="submit" type="submit" value="Submit">
                 </td>
               </tr>
             </table>
           </td>
         </tr>
       </tbody>
     </table>
 
   </form>
 </div>
 
 <script src="/js/jquery.min.js"></script>
 <script>
   var table_template = ''
     + '<table class="entries"><tbody><tr><td>'
     + '<h2>Metadata</h2>'
     + '<input type="hidden" name="numtable" value="{0}">'
     + '<table class="formtable" id="formtable_{0}">'
     + '<tr>'
     + '<td>Title of article:</td>'
     + '<td><input name="title_{0}" type="text" '
     + 'value="">'
     + '<br>'
     + '<span class="example">Example: <em>Example Submission</em></span>'
     + '</td>'
     + '</tr>'
     + '<tr>'
     + '<td>Short article name (folder name):</td>'
     + '<td><input name="shortname_{0}" type="text"'
     + 'value="">'
     + '<br>'
     + '<span class="example">Example: <em>Example_Submission</em> (name of the folder where'
     + 'your ROOT and theory files reside)'
     + '</span>'
     + '</td>'
     + '</tr>'
     + '<tr>'
     + '<td>Authors:</td>'
     + '<td><input name="author_{0}" type="text"'
     + 'value="">'
     + '<br>'
     + '<span class="example">'
     + 'Example:'
     + '<em>'
-    + 'Gerwin Klein &lt;http://www.cse.unsw.edu.au/~kleing/&gt;,'
+    + 'Gerwin Klein &lt;https://www.cse.unsw.edu.au/~kleing/&gt;,'
     + 'Johannes H&ouml;lzl &lt;mailto:hoelzl@in.tum.de&gt;'
     + '</em>'
     + '</span>'
     + '</td>'
     + '</tr>'
     + '<tr>'
     + '<td>Topics:</td>'
     + '<td><input name="topic_{0}" type="text"'
     + 'value="">'
     + '<br>'
     + '<span class="example">'
     + 'Example: <em>Computer Science/Security, '
     + 'Computer Science/Programming, Languages/Type Systems</em><br>'
-    + '(<a href=http://www.isa-afp.org/topics.shtml>Index of topics</a>)'
+    + '(<a href=https://www.isa-afp.org/topics.shtml>Index of topics</a>)'
     + '</span>'
     + '</td>'
     + '</tr>'
     + '<tr>'
     + '<td>License:</td>'
     + '<td><label><input type="radio" name="license_{0}" value="BSD"'
     + 'checked>BSD</label>'
     + '<label><input type="radio" name="license_{0}" value="LGPL"'
     + '>LGPL</label>'
     + '<br>'
     + '<span class="example">'
     + 'Note: For LGPL submissions, please include the header "License: LGPL" in each file'
     + '</span>'
     + '</td>'
     + '</tr>'
     + '<tr>'
     + '<td>Abstract:</td>'
     + '<td><textarea name="abstract_{0}"></textarea>'
     + '<br>'
     + '<span class="example">'
     + 'Note: You can use HTML to format your abstract.'
     + '</span>'
     + '</td>'
     + '</tr>'
     + '</table>'
     + '<p>'
     + '<a href="javaScript:void(0);" class="removeField">Remove this entry</a>'
     + '</p>'
     + '</td></tr></tbody></table>'
     + '<p>&nbsp;</p>'
     + '';
   var regex = new RegExp('\\{0\\}', 'g');
   function noOfFields() {
     var noOfForms = $.map($(".formtable"), function (val, i) {
       return parseInt(val.id.replace('formtable_', ''));
     });
     return Math.max.apply(0, noOfForms);
   }
   $("#newFields").click(function () {
     $(this).closest(".entries").before(table_template.replace(regex, String(noOfFields() + 1)));
   });
   $("#rightbox").on("click", ".removeField", function () {
     $(this).closest(".entries").remove();
   });
   $(".hide-button").click(function () {
     $("#hide-toggle").toggleClass("active");
     $("#hide").slideToggle();
   })
 </script>
 <style type="text/css">
   input[type=text] {
     width: 30em;
   }
 
   .red {
     color: red;
     font-size: 0.7em;
   }
 
   .example {
     font-size: 0.8em;
   }
 
   textarea {
     width: 40em;
     height: 15em;
   }
 
   h1 {
     font: small-caps bold large sans-serif;
   }
 
   h2 {
     font-size: 1.2em;
     margin: 0.5em 0.2em 0 0.2em;
     padding: 0;
   }
 
   td {
     vertical-align: top;
   }
 
   tr.archive_table_row td {
     padding-top: 1.5em;
   }
 
   code {
     background-color: #F2F2F2;
     color: #303030;
     padding: 1px 2px 2px 2px;
     border-radius: 4px;
   }
 
   #log {
     width: 85%;
     background: white;
     margin: auto;
     border: thin solid;
     padding: 5px;
   }
 
   .log_button {
     width: 20em;
   }
 
   .formtable tr td:first-child {
     width: 8em;
   }
 
   .formtable td {
     padding: 0.4em;
   }
 
   #formtable_end tr td:first-child {
     width: 8em;
   }
 
   #formtable_end td {
     padding: 0.4em;
   }
 
   input[type="file"] {
     font-weight: bold;
   }
 
   #hide-toggle {
     cursor: pointer;
   }
 
   #hide-toggle:before {
     content: "▾ ";
   }
 
   #hide-toggle.active:before {
     content: "▸ ";
   }
 </style>
\ No newline at end of file
diff --git a/admin/site/themes/afp/theme.toml b/admin/site/themes/afp/theme.toml
--- a/admin/site/themes/afp/theme.toml
+++ b/admin/site/themes/afp/theme.toml
@@ -1,21 +1,21 @@
 # theme.toml template for a Hugo theme
 # See https://github.com/gohugoio/hugoThemes#themetoml for an example
 
 name = "Afp"
 license = "MIT"
-licenselink = "https://github.com/yourname/yourtheme/blob/master/LICENSE"
+licenselink = "https://www.isa-afp.org/LICENSE"
 description = ""
-homepage = "http://example.com/"
+homepage = "https://isa-afp.org/"
 tags = []
 features = []
 min_version = "0.41"
 
 [author]
   name = ""
   homepage = ""
 
 # If porting an existing theme
 [original]
   name = ""
   homepage = ""
   repo = ""