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,64 +1,64 @@
 ---
 title: Entry Submission
 menu: 
     main:
         name: "Submission"
         weight: 5
 ---
 
 ## Submission Guidelines
 
 **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
+## 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](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/assets/sass/main.scss b/admin/site/themes/afp/assets/sass/main.scss
--- a/admin/site/themes/afp/assets/sass/main.scss
+++ b/admin/site/themes/afp/assets/sass/main.scss
@@ -1,1164 +1,1169 @@
 //colors
 $theme: hsl(242, 27%, 24%);
 $theme-hover: hsl(241, 26%, 36%);
 $theme-lightest: hsl(261, 36%, 86%);
 $theme-focus: #acabcf;
 $link: #0645ad;
 $link-hover: #0000ee;
 $link-visited: #42047c;
 $white: #fff;
 $lightest-grey: #f2f2f2;
 $lighter-grey: #ddd;
 $light-grey: #bbb;
 $dark-grey: #777;
 $darker-grey: #555;
 $darkest-grey: #303030;
 $black: #000;
 $black_15: rgba(0, 0, 0, 0.15);
 
 //fonts
 $sans-serif: "Open Sans", sans-serif;
 $monospace: "Consolas", monospace;
 $OpenSans: "Open Sans";
 
 $light: 300;
 $normal: 400;
 $bold: 700;
 
 $border-bottom: 2px $darker-grey solid;
 
 //sizes
 $size-xs: 650px; // for example mobile
 $size-s: 875px; // for example half desktop window
 $size-xl: 1800px; // for example 4k desktop
 
 %code {
   font-family: $monospace;
   background-color: $lightest-grey;
   color: $darkest-grey;
 }
 
 %button {
   border: 1px solid $dark-grey;
   font-size: 1rem;
   vertical-align: middle;
   background-color: $white;
   color: $black;
   line-height: 0;
   font-family: $sans-serif;
 }
 
 %button-image {
   position: relative;
   top: 0.12em;
   left: 5px;
   padding-right: 5px;
 }
 
 %sticky {
   position: sticky;
   top: 0;
   background-color: $white;
   margin: 0;
   padding-bottom: 0.5rem;
 }
 
 @font-face {
   font-family: $OpenSans;
   font-display: swap;
   font-style: normal;
   font-weight: 300;
   src: local(""), url("/font/open-sans-v18-latin-300.woff2") format("woff2"),
   url("/font/open-sans-v18-latin-300.woff") format("woff");
 }
 
 @font-face {
   font-family: $OpenSans;
   font-display: swap;
   font-style: normal;
   font-weight: 400;
   src: local(""), url("/font/open-sans-v18-latin-regular.woff2") format("woff2"),
   url("/font/open-sans-v18-latin-regular.woff") format("woff");
 }
 
 @font-face {
   font-family: $OpenSans;
   font-display: swap;
   font-style: italic;
   font-weight: 400;
   src: local(""), url("/font/open-sans-v18-latin-italic.woff2") format("woff2"),
   url("/font/open-sans-v18-latin-italic.woff") format("woff");
 }
 
 @font-face {
   font-family: $OpenSans;
   font-display: swap;
   font-style: normal;
   font-weight: 700;
   src: local(""), url("/font/open-sans-v18-latin-700.woff2") format("woff2"),
   url("/font/open-sans-v18-latin-700.woff") format("woff");
 }
 
 @font-face {
   font-family: $OpenSans;
   font-display: swap;
   font-style: italic;
   font-weight: 700;
   src: local(""), url("/font/open-sans-v18-latin-700italic.woff2") format("woff2"),
   url("/font/open-sans-v18-latin-700italic.woff") format("woff");
 }
 
 *::selection {
   background-color: $theme;
   color: $white;
 }
 
 body {
   color: $black;
   background: $white;
   font-family: $sans-serif;
   display: grid;
   grid-template-columns: #{"max(20%, 200px)"} 1fr;
   grid-template-areas: "sidebar content";
   justify-items: center;
   margin: 0;
 }
 
 aside {
   grid-area: sidebar;
   background-color: $theme;
   width: 20vw;
   margin: 0;
   height: 100%;
   position: fixed;
   top: 0;
   left: 0;
   min-width: 200px;
   word-break: break-all;
   overflow-y: auto;
   color: $white;
 
   nav {
     display: flex;
     flex-direction: column;
     justify-content: space-between;
     height: 100vh;
   }
 
   ul {
     list-style: none;
     padding: 0;
   }
 
   li {
     padding: 0.5em 2rem;
 
     &:hover {
       background-color: $theme-hover;
     }
   }
 
   .active {
     background-color: $theme-hover;
   }
 
   div > a {
     display: block;
     text-align: center;
   }
 
   a:not(.entity_ref) {
     &.link,
     &:link,
     &:visited {
       color: $white;
     }
 
     &:focus {
       outline: 1px $theme-focus solid;
       outline-offset: 3.5px;
     }
   }
 
   hr {
     margin: 2rem;
     border: none;
     border-top: 2px solid $dark-grey;
   }
 }
 
 .logo {
   width: 40%;
   height: auto;
   padding: 10%;
   max-width: 160px;
 }
 
 li {
   margin: 0.25em 0;
 }
 
 header {
   border-bottom: $border-bottom;
   margin-bottom: 20px;
   padding: 0.5rem 0;
 
   > div {
     display: flex;
     justify-content: space-between;
     padding: 0.5rem 0;
   }
 
   form {
     padding: 0.5rem 0;
     float: right;
   }
 
   h1 {
     padding: 0.5rem 0;
     margin: 0;
     clear: both;
     line-height: 2.75rem;
   }
 
   #search-input {
     height: 2rem;
     padding: 7px;
     width: 175px;
   }
 
   #search-button {
     height: 2rem;
     padding: 7px;
     width: 2rem;
 
     &:hover {
       background-color: $lighter-grey;
     }
 
     &:active {
       background-color: $light-grey;
     }
   }
 
   div p {
     margin: 0;
   }
 }
 
 .content {
   grid-area: content;
   margin: 0 auto 2rem;
   width: #{"min(80%, 1100px)"};
   min-width: 550px;
 
   div {
     line-height: 1.35em;
     width: 100%;
 
     h1 {
       border-bottom: $border-bottom;
     }
   }
 
   > div {
     form {
       margin: 2rem auto 0;
       width: 50%;
       min-width: 290px;
       padding: 1rem 0;
     }
 
     #search-button {
       height: 2.5rem;
       width: 25%;
       min-width: 70px;
       background: $theme;
       color: $white;
       border: 1px $theme solid;
     }
 
     #search-input {
       height: 2.5rem;
       width: 75%;
     }
   }
 
   .popup {
     background: $white;
     box-shadow: 0 0 8px 0 $black_15, 0 4px 10px 0 $black_15;
     padding: 2.5rem;
     display: block;
     width: auto;
     min-width: 300px;
     max-width: 90vw;
     max-height: 75vh;
     position: fixed;
     left: 50%;
     top: 50%;
     transform: translate(-50%, -50%);
     overflow-y: auto;
   }
 
   .chart {
     min-width: 400px;
     width: 100%;
     min-height: 400px;
     max-height: 50vh;
     background: $white;
     margin: 20px auto 40px;
     border: 1px solid $black;
     position: relative;
   }
 
   .statsnumber {
     text-align: right;
     padding-right: 1rem;
   }
 
   ul {
     list-style-type: none;
   }
 
   li {
     word-wrap: break-word;
     word-break: break-word;
   }
 
-  li::before {
+  dt {
+    font-weight: $light;
+    margin-top: 0.5em;
+  }
+
+  ul > li::before {
     content: "–";
     position: absolute;
     margin-left: -1.3em;
   }
 }
 
 .entries {
   > div {
     display: grid;
     grid-template-columns: 3fr 1fr;
   }
 
   main {
     padding-right: 2%;
     max-width: 90ch;
 
     div {
       margin: 1rem 0;
     }
   }
 
   nav {
     width: 130px;
     margin-left: auto;
 
     h4 {
       color: $darker-grey;
       font-weight: $normal;
     }
   }
 }
 
 .theories {
   grid-template-columns: 20% 80%;
   justify-content: normal;
 
   .collapsible.collapsed {
     display: none;
   }
 
   .invertible.collapsed {
     transform: scale(1, -1);
   }
 
   .collapse-container.collapsed {
     .collapsible {
       display: none;
     }
 
     .invertible {
       transform: scale(1, -1);
     }
   }
 
   .content {
     min-width: clamp(60ch, 50vw, 50vw);
     width: 100%;
     max-width: 75vw;
     margin: 0 0 2rem 4vw;
   }
 
   pre {
     width: fit-content;
   }
 
   h2 {
     @extend %sticky;
     padding-top: 0.5rem;
     border-bottom: 1px $light-grey solid;
 
     svg {
       height: 2rem;
       width: 20px;
       position: sticky;
       right: 1rem;
       float: right;
       stroke: $dark-grey;
       transition: transform 100ms;
     }
   }
 
   main {
     > div {
       margin-bottom: 1rem;
     }
   }
 
   aside {
     word-break: normal;
     z-index: 1;
     overflow-x: hidden;
 
     .logo {
       padding-top: 2rem;
       padding-bottom: 2rem;
       width: 100px;
 
       @media screen and (min-width: $size-xl) {
         width: 150px;
       }
     }
 
     #return {
       position: sticky;
       top: 0rem;
       background: #2E2D4E;
       min-width: 200px;
     }
 
     #pdfs {
       position: fixed;
       bottom: 0;
       background: #2E2D4E;
       margin: 0;
       padding: 1rem 1.75rem;
       width: 20vw;
       box-sizing: border-box;
       cursor: pointer;
     }
 
     > div {
       margin-right: 1rem;
     }
 
     &:hover {
       min-width: fit-content;
 
       div {
         min-width: fit-content;
       }
     }
 
     ul {
       margin-left: 1.75rem;
     }
 
     li {
       padding: 0;
 
       &:hover {
         background-color: $theme;
       }
 
       > a:hover {
         background-color: $theme-hover;
       }
 
       a {
         padding: 0.5em 0;
         display: inline-block;
         width: 100%;
       }
     }
   }
 
   @media screen and (max-width: $size-s) {
     padding: 0;
     grid-template-columns: 1fr;
 
     aside {
       overflow-x: visible;
     }
 
     #menu {
       min-width: fit-content;
       padding-right: 1rem;
     }
 
     .content {
       min-width: 350px;
       max-width: 100vw;
       margin: 80px 0 0 20px;
     }
 
     h2 {
       top: 80px;
       padding-left: 0.5rem;
     }
   }
 }
 
 .links {
   button {
     display: inline-block;
     margin: 0.5rem 0;
   }
 
   a {
     display: inline-block;
     margin: 0.5rem 0;
   }
 }
 
 .popup-button:not(.entity_ref) {
   &:visited {
     color: $white;
   }
 
   &.link,
   &:link {
     border: none;
     padding: 0.75rem 0;
     background-color: $theme;
     color: $white;
     cursor: pointer;
     text-align: center;
     transition: background-color 200ms ease, transform 150ms ease;
     font-weight: $bold;
     font-size: 0.9rem;
     width: 130px;
   }
 
   &:active {
     transform: scale(0.98);
   }
 }
 
 a:not(.entity_ref) {
   &.link,
   &:link {
     color: $link;
     text-decoration: none;
     font-weight: $bold;
   }
 
   &:visited {
     color: $link-visited;
   }
 
   &:hover {
     color: $link-hover;
   }
 }
 
 h1 {
   margin: 1.5em 0 0 0;
   font-size: 2em;
   padding-bottom: 20px;
 
   span.first {
     font-size: 2.3rem;
   }
 }
 
 h2 {
   margin: 1.5em 0 0 0;
   padding: 0;
   line-height: normal;
 }
 
 h3 {
   margin: 1.5em 0 0 0;
   font-stretch: normal;
   font-size: larger;
   padding: 0;
   font-weight: $light;
 
   &:first-child {
     margin: 0.5rem 0 0 0;
   }
 }
 
 h4 {
   margin: 1.5em 0 0 0;
   margin-bottom: 0.5ex;
   font-weight: $bold;
 }
 
 .popup {
   h2 {
     margin-top: 0;
   }
 
   .close {
     position: absolute;
     width: 20px;
     height: 20px;
     top: 2rem;
     right: 2rem;
     transition: all 200ms;
     font-size: 24px;
     font-weight: $bold;
     color: $darker-grey;
     text-align: center;
 
     &:hover {
       color: $darkest-grey;
     }
   }
 }
 
 #download-popup {
   a[download] {
     display: block;
     width: 154px;
     margin: 2.5rem auto 0;
   }
 }
 
 .year {
   @extend %sticky;
   padding-top: 2rem;
   border-bottom: $border-bottom;
 }
 
 img {
   max-width: 90%;
 }
 
 pre {
   @extend %code;
   padding: 1rem;
   overflow: auto;
 
   &.bibtex {
     white-space: pre;
     border-width: thin;
     border-style: solid;
   }
 
   &.code {
     white-space: pre;
     padding: 10px 2px;
   }
 }
 
 code {
   padding: 1px 2px 2px;
   @extend %code;
 }
 
 blockquote {
   border: 2px solid $lighter-grey;
   padding: 1rem 2rem;
   margin: auto 0;
 }
 
 tr:nth-child(even) {
   background-color: $lightest-grey;
 }
 
 .nobr {
   white-space: nowrap;
 }
 
 .large-top-margin {
   margin-top: 48px;
 }
 
 .search-page {
   > div {
     display: grid;
     grid-template-columns: 3fr #{"max(25%, 175px)"};
     grid-template-rows: 150px 1fr;
     grid-template-areas:
       "search search"
       "entries sidebar";
   }
 
   form {
     grid-area: search;
   }
 
   #search-main {
     grid-area: entries;
     padding-right: 2rem;
     box-sizing: border-box;
   }
 
   #search-results {
     > div {
       position: relative;
       margin: 1.5rem 0;
       border-bottom: 2px $lighter-grey solid;
       padding-bottom: 1.5rem;
     }
 
     div + div {
       margin-top: 1rem;
     }
 
     .title,
     .subtitle {
       display: flex;
       justify-content: space-between;
       align-items: center;
     }
 
     .subtitle {
       color: $dark-grey;
       font-size: 0.875em;
 
       > p {
         margin: 0;
       }
     }
 
     a[download] {
       padding: 5px 7.5px;
       flex-shrink: 0;
       margin-left: 1em;
     }
   }
 
   #search-sidebar {
     grid-area: sidebar;
   }
 }
 
 a[download] {
   display: inline-block;
   color: $black;
   height: 22px;
   padding: 4px 7px;
   @extend %button;
 
   &:focus {
     outline: none;
     box-shadow: 0 0 0 2px #c5c4ddbb;
   }
 
   &:hover,
   &:active {
     background-color: $light-grey;
     color: $black;
   }
 
   &:after {
     content: url("/images/download.svg");
     @extend %button-image;
   }
 }
 
 .entry {
   display: flex;
   align-items: center;
   margin-top: 1.35rem;
 
   a[download] {
     position: absolute;
     top: 0;
     right: 0;
   }
 
   .date {
     text-align: right;
     width: 15%;
     min-width: 6ch;
     font-family: $monospace;
   }
 
   h5 {
     font-size: initial;
     display: initial;
   }
 }
 
 .form-container {
   width: 290px;
   text-align: left;
 }
 
 #search-input {
   @extend %button;
   border-right: none;
   font-family: $sans-serif;
   padding: 0.5em;
 }
 
 #search-button:not(.entity_ref) {
   @extend %button;
   cursor: pointer;
 
   &:focus {
     outline: none;
     box-shadow: 0 0 0 2px #c5c4ddbb;
   }
 
   img {
     max-width: 1rem;
   }
 }
 
 .entity_def.active {
   background-color: $theme-focus;
 }
 
 button {
   @extend %button;
   height: 2rem;
   padding: 7px;
   font-weight: $bold;
   cursor: pointer;
 
   &:hover {
     background-color: $lighter-grey;
   }
 
   &:active {
     background-color: $light-grey;
   }
 
   &:focus {
     outline: none;
     box-shadow: 0 0 0 2px #c5c4ddbb;
   }
 }
 
 button[copy] {
   &:after {
     content: url("/images/copy.svg");
     @extend %button-image;
   }
 }
 
 #search-input-autocomplete-list {
   width: 214px;
   position: absolute;
   margin-bottom: 24px;
   padding: 8px 0;
   background-color: $white;
   border: 1px solid $lighter-grey;
   box-shadow: 0 2px 4px $black_15;
   z-index: 1;
 
   div {
     width: auto;
     padding: 8px 12px;
     line-height: 16px;
     cursor: pointer;
 
     &:hover {
       background: $lighter-grey;
     }
   }
 }
 
 .autocomplete-active {
   background: $lighter-grey;
 }
 
 .item-text {
   width: 85%;
 }
 
 .date {
   color: $darker-grey;
   font-size: 14px;
 }
 
 .overlay {
   position: fixed;
   top: 0;
   bottom: 0;
   left: 0;
   right: 0;
   background: $black_15;
   transition: opacity 200ms;
   visibility: hidden;
   opacity: 0;
 
   .cancel {
     position: absolute;
     width: 100%;
     height: 100%;
     cursor: pointer;
   }
 
   &:target {
     visibility: visible;
     opacity: 1;
   }
 }
 
 .status-ok {
   background-color: #00FF99;
   padding: 8px;
 }
 
 .status-skipped {
   background-color: #FFFF99;
   padding: 8px;
 }
 
 .status-failed {
   background-color: #DD2222;
   padding: 8px;
 }
 
 iframe {
   width: 100%;
   height: 90vh;
 }
 
 .loader {
   margin: 24px 24px 0 0;
   height: 6px;
   position: relative;
   display: block;
   background-color: $theme;
   border-radius: 4px;
   overflow: hidden;
 
   .animation {
     background-color: $light-grey;
 
     &:before {
       content: '';
       position: absolute;
       background-color: inherit;
       top: 0;
       left: 0;
       bottom: 0;
       will-change: left, right;
       animation: loader 2s linear infinite;
     }
   }
 }
 
 .obfuscated {
   -webkit-user-select: none;
   -moz-user-select: none;
   -ms-user-select: none;
   user-select: none;
 }
 
 .rev {
   unicode-bidi: bidi-override;
   direction: rtl;
 }
 
 @keyframes loader {
   0% {
     left: -20%;
     right: 100%;
   }
   100% {
     left: 100%;
     right: -20%;
   }
 }
 
 #menu-toggle {
   input,
   label {
     display: none;
   }
 
   > .logo-link, img[alt="Search"] {
     display: none;
   }
 
   form {
     display: none;
   }
 }
 
 @media screen and (max-width: $size-xs) {
   .content {
     width: 90%;
     min-width: 350px;
   }
 
   .search-page {
     > div {
       display: grid;
       grid-template-columns: 1fr;
       grid-template-rows: 150px auto auto;
       grid-template-areas:
         'search'
         'sidebar'
         'entries';
     }
   }
 }
 
 @media screen and (min-width: $size-s) {
   ul.horizontal-list {
     display: flex;
     flex-flow: wrap;
     padding-left: 0;
 
     li {
       margin-right: 16px;
     }
 
     li::before {
       content: none;
     }
   }
 }
 
 @media screen and (max-width: $size-s) {
   body {
     grid-template-columns: 1fr;
     grid-template-areas: 'content';
   }
 
   aside {
     height: 80px;
     width: 100vw;
     overflow-y: visible;
     z-index: 1;
   }
 
   header {
     form {
       display: none;
     }
   }
 
   .content {
     margin-top: 80px;
   }
 
   .entries {
     > div {
       display: grid;
       grid-template-rows: auto auto;
       grid-template-columns: 1fr;
     }
 
     nav {
       margin-left: 0;
     }
   }
 
 
   .large-top-margin {
     margin-top: 0;
   }
 
   #banner {
     left: 0;
     width: 100vw;
     height: 75px;
 
     p {
       line-height: normal;
       margin: 1rem;
     }
   }
 
   #menu-toggle {
     background: $theme;
     display: block;
     position: relative;
     top: 0;
     left: 0;
     z-index: 1;
     height: 80px;
     user-select: none;
     width: 100vw;
 
     a {
       text-decoration: none;
       transition: color 0.3s ease;
     }
 
     .logo-link {
       height: 3rem;
       max-width: 50vw;
       top: 1rem;
       left: 0;
       right: 0;
       margin-left: auto;
       margin-right: auto;
 
       img {
         padding: 0;
         height: 3rem;
         object-fit: contain;
       }
     }
 
     .logo-link, input, label, a[href="/search"] {
       display: block;
       position: absolute;
       z-index: 2;
     }
 
     input, label, a[href="/search"] {
       width: 24px;
       height: 24px;
       top: 28px;
     }
 
     input, label {
       left: 28px;
       cursor: pointer;
     }
 
     a[href="/search"] {
       right: 28px;
       filter: invert(1);
     }
 
     a[href="/search"] img, label img {
       width: 100%;
     }
 
     input {
       opacity: 0;
 
       &:checked {
         ~ nav {
           left: 0;
         }
       }
     }
 
     label span {
       display: none;
     }
   }
   #menu {
     box-shadow: 0 .5rem 1rem rgba(0, 0, 0, .15);
     height: calc(100vh - 80px);
     position: absolute;
     top: 0;
     margin-top: 80px;
     box-sizing: border-box;
     min-width: 200px;
     width: 50vw;
     max-width: 350px;
     min-height: 355px;
     background: $theme;
     left: -100%;
     transition: left 0.3s ease;
     overflow-y: scroll;
 
     .logo-link {
       display: none;
     }
   }
 }
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,197 +1,201 @@
 {{- 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") -}}
+
+  <h3>License</h3>
+  <div>
+  {{- if (eq .Params.license "BSD") -}}
   <a href="https://isa-afp.org/LICENSE">BSD License</a>
   {{- else if (eq .Params.license "LGPL") -}}
   <a href="https://isa-afp.org/LICENSE.LGPL">GNU Lesser General Public License (LGPL)</a>
   {{- else -}}
     {{- printf "%s License" .Params.license -}}
   {{- end -}}
+  </div>
 
   {{- with .Params.note -}}
   <p><em>{{ . }}</em></p>
   {{- end -}}
 
   {{- with.Params.history -}}
-  <h3>Change history</h3>
+  <h3>History</h3>
+  <dl>
   {{- range . -}}
-    <p>
-    <h4>{{ dateFormat "January 2, 2006" .date }}</h4>
-    {{ safeHTML .value }}
-    </p>
+    <dt>{{ dateFormat "January 2, 2006" .date }}</dt>
+    <dd>{{ safeHTML .value }}</dd>
   {{- end -}}
+  </dl>
   {{- end -}}
 
   {{- with .Params.extra -}}
   {{- range $key, $value := . -}}
   <h3>{{- humanize $key -}}</h3>
 
   <p>{{- $value | safeHTML -}}</p>
   {{- end -}}
   {{- end -}}
 
   {{- $Scratch := newScratch -}}
   
   {{- with .Params.topics -}}
   <h3>Topics</h3>
   <ul>
     {{- range . -}}
     <li>{{- printf "[%s](/topics/%s)" . (urlize .) | $.Page.RenderString -}}</li>
     {{- end -}}
   </ul>
   {{- end -}}
 
   {{- with .Params.related -}}
-  <h3>Related Publications</h3>
+  <h3>Related publications</h3>
   <ul>
   {{- range . -}}
     <li>
       {{ safeHTML . }}
     </li>
   {{- end -}}
   </ul>
   {{- end -}}
 
   {{- range .Params.sessions -}}
   {{ $session := .session }}
-  <h3>Theories of {{ $session }}</h3>
+  <h3>Session {{ $session }}</h3>
   <ul>
     {{- range .theories }}
     <li><a href="/theories/{{ urlize $session }}/#{{ . }}">{{ . }}</a></li>
     {{- end -}}
   </ul>
   {{- end -}}
 
   <div class="flex-wrap">
   {{ $uses := .Params.dependencies }}
   {{- with $uses -}}
   <div>
-    <h3>Depends On</h3>
+    <h3>Depends on</h3>
     <ul class="horizontal-list">
       {{- range . -}}
       {{- $path := printf "/entries/%s.html" . -}}
       {{- with $site.Site.GetPage $path -}}
       <li>{{- printf "[%s](%s)" .Title $path | $.Page.RenderString -}}</li>
       {{- end -}}
       {{- end -}}
     </ul>
   </div>
   {{- end -}}
 
   {{- $used_by := (index .Site.Taxonomies.dependencies (urlize $entry_name)) -}}
   {{- with $used_by -}}
   <div>
     <h3>Used by</h3>
     <ul class="horizontal-list">
       {{- range . -}}
       <li>{{- printf "[%s](%s)" .Title .RelPermalink | $.Page.RenderString -}}</li>
       {{- end -}}
     </ul>
   </div>
   {{- end -}}
   
   {{ $related :=
     (where (.Site.RegularPages.Related .) ".File.BaseFileName" "not in" $uses)
     | complement $used_by
     | first 5 }}
   {{ with $related }}
   <div>
-    <h3>Related Entries</h3>
+    <h3>Auto-related entries</h3>
     <ul class="horizontal-list">
       {{ range . }}
       <li>{{- printf "[%s](%s)" .Title .RelPermalink | $.Page.RenderString -}}</li>
       {{ end }}
     </ul>
   </div>
   {{ end }}
   </div>
 </main>
 
 <nav class='links'>
   <a class='popup-button' href="#cite-popup">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>
 
   {{- if isset .Site.Data "status" -}}
   {{- $status := "none" -}}
   {{- range where .Site.Data.status.entries "entry" $entry_name -}}
   {{- $status = .status -}}
   {{- end -}}
-  <h4>Build Status</h4>
+  <h4>Build status</h4>
   <div class="status-{{ $status }}">
   <strong>{{- $status -}}</strong>
   <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>
   <a href="{{ .Site.Data.status.build_data.url }}">{{ .Site.Data.status.build_data.job }}</a>
   </div>
   {{- end -}}
 </nav>
 
 <div id="cite-popup" 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="bibtex-filename">{{- $entry_name -}}-AFP</p>
       {{- $authors := slice }}
       {{- range .Params.authors -}}
         {{- $authors = $authors | append (index (index $site.Site.Data.authors .) "name") -}}
       {{- end -}}
       <pre id="copy-text">@article{{- "{" -}}{{- $entry_name -}}-AFP,
   author  = {{ "{" -}}{{- delimit $authors " and " -}}},
   title   = {{ "{" -}}{{- htmlUnescape .Params.title -}}},
   journal = {Archive of Formal Proofs},
   month   = { {{- dateFormat "January" .Params.date -}} },
   year    = { {{- dateFormat "2006" .Params.date -}} },
   note    = {\url{https://isa-afp.org/entries/{{- $entry_name -}}.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }</pre>
       <button id="copy-bibtex">Copy</button> <a id="download-bibtex">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="{{ $site.Site.Params.afpUrls.releases }}//afp-{{- $entry_name -}}-current.tar.gz" download>Download latest</a>
     {{ with .Params.releases -}}
     <p>Older releases:</p>
     <ul>
       {{- range . -}}
       <li>
         <a href="{{ $site.Site.Params.afpUrls.releases }}/afp-{{- $entry_name -}}-{{- .date -}}.tar.gz">
           {{- dateFormat "Jan 2, 2006" .date -}}
         </a>: Isabelle{{ .isabelle }}
       </li>
       {{- end -}}
     </ul>
     {{- end }}
   </div>
 </div>
 
 {{- end -}}
diff --git a/admin/site/themes/afp/layouts/shortcodes/statistics.html b/admin/site/themes/afp/layouts/shortcodes/statistics.html
--- a/admin/site/themes/afp/layouts/shortcodes/statistics.html
+++ b/admin/site/themes/afp/layouts/shortcodes/statistics.html
@@ -1,185 +1,185 @@
 <table>
   <tr>
     <td class="statsnumber">{{ len (where .Site.RegularPages "Section" "==" "entries") }}</td>
     <td><a href="/">Entries</a></td>
   </tr>
   <tr>
     <td class="statsnumber">{{ len $.Site.Taxonomies.authors }}</td>
     <td><a href="/authors/">Authors</a></td>
   </tr>
   <tr>
     <td class="statsnumber">~{{ lang.NumFmt 0 (mul (math.Round (div .Site.Data.statistics.num_lemmas 100)) 100) }}</td>
     <td>Lemmas</td>
   </tr>
   <tr>
     <td class="statsnumber">~{{ lang.NumFmt 0 (mul (math.Round (div .Site.Data.statistics.num_loc 100)) 100) }}</td>
     <td>Lines of Code</td>
   </tr>
 </table>
 
-<h4>Most used AFP articles:</h4>
+<h4>Most used AFP entries:</h4>
 <table id="most_used">
   <tr>
     <th></th>
     <th>Name</th>
-    <th>Used by ? articles</th>
+    <th>Used by ? entries</th>
   </tr>
 
   {{ range $index, $element := first 12 .Site.Taxonomies.dependencies.ByCount }}
   <tr>
     <td>{{ add $index 1}}.</td>
     <td><a href="/entries/{{- $element.Page.Title -}}.html">{{ $element.Page.Title }}</a></td>
     <td><a href="{{- $element.Page.RelPermalink -}}">{{ $element.Count }}</a></td>
   </tr>
   {{ end }}
 </table>
 
 <script>
   const years = [{{- delimit .Site.Data.statistics.years "," | safeJS -}}]
   const no_articles = [{{- delimit .Site.Data.statistics.articles_year "," | safeJS -}}]
   const no_loc = [{{- delimit .Site.Data.statistics.loc_years  "," | safeJS -}} ]
   const no_authors = [{{- delimit .Site.Data.statistics.author_years  "," | safeJS -}}]
   const no_authors_series = [{{- delimit .Site.Data.statistics.author_years_cumulative  "," | safeJS -}}]
   const all_articles = [{{- delimit (apply .Site.Data.statistics.all_articles "printf" "'%s'" ".") "," | safeJS -}}]
   const article_years_unique = [{{- delimit (apply .Site.Data.statistics.article_years_unique "printf" "'%s'" ".") "," | safeJS -}}]
   const loc_articles = [{{- delimit .Site.Data.statistics.loc_articles "," | safeJS -}}]
 </script>
-<h4>Growth in number of articles:</h4>
+<h4>Growth in number of entries:</h4>
 <script src="/js/Chart.js"></script>
 <div class="chart">
   <canvas id="num-articles-canvas"></canvas>
 </div>
 <script>
   new Chart(document.getElementById("num-articles-canvas"), {
     type: 'bar',
     data: {
       labels: years,
       datasets: [{
-        label: 'size of the AFP in # of articles',
+        label: 'Size of the AFP in # of entries',
         data: no_articles,
         backgroundColor: "rgba(46, 45, 78, 1)"
       }],
     },
     options: {
       responsive: true,
       maintainAspectRatio: false,
       scales: {
         yAxes: [{
           ticks: {
             beginAtZero: true
           }
         }]
       },
     }
   })
 </script>
 
 <h4>Growth in lines of code:</h4>
 <div class="chart">
   <canvas id="loc-years-canvas"></canvas>
 </div>
 <script>
   new Chart(document.getElementById("loc-years-canvas"), {
     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: false,
       scales: {
         yAxes: [{
           ticks: {
             beginAtZero: true
           }
         }]
       },
     }
   })
 </script>
 
 <h4>Growth in number of authors:</h4>
 <div class="chart">
   <canvas id="author-years-canvas"></canvas>
 </div>
 <script>
   new Chart(document.getElementById("author-years-canvas"), {
     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: false,
       scales: {
         yAxes: [{
           ticks: {
             beginAtZero: true
           }
         }]
       },
     }
   })
 </script>
 
-<h4>Size of articles:</h4>
+<h4>Size of entries:</h4>
 <div class="chart">
   <canvas id="loc-articles-canvas"></canvas>
 </div>
 <script>
   new Chart(document.getElementById("loc-articles-canvas"), {
     type: 'bar',
     data: {
       labels: article_years_unique,
       datasets: [{
         label: 'loc per article',
         data: loc_articles,
         backgroundColor: 'rgba(101, 99, 136, 1)'
       }]
     },
     options: {
       responsive: true,
       maintainAspectRatio: false,
       scales: {
         xAxes: [{
           categoryPercentage: 1,
           barPercentage: 0.9,
           ticks: {
             autoSkip: false
           }
         }],
         yAxes: [{
           ticks: {
             beginAtZero: true
           }
         }]
       },
       tooltips: {
         callbacks: {
           title: tooltipItem => all_articles[tooltipItem[0].index]
         }
       }
     }
   })
 </script>
 
 </td>
 </tr>
 
 </tbody>
 </table>
\ No newline at end of file
diff --git a/admin/site/themes/afp/layouts/topics/list.html b/admin/site/themes/afp/layouts/topics/list.html
--- a/admin/site/themes/afp/layouts/topics/list.html
+++ b/admin/site/themes/afp/layouts/topics/list.html
@@ -1,36 +1,35 @@
 {{ define "main" }}
 {{- $site := . -}}
 {{- $topic := .Site.Data.topics -}}
 
 {{- range (split .Title "/") -}}
 {{- with $topic.topics -}}
 {{- $topic = $topic.topics}}
 {{- end -}}
 {{- $topic = index $topic . -}}
 {{- end -}}
 
 {{- with $topic.classification -}}
 <h2>Subject Classification</h2>
 {{- range . -}}
-<h3>{{ .type }}</h3>
-<a href="{{ .url }}">{{ .desc }}</a>
+<p>{{ .type }}: <a href="{{ .url }}">{{ .desc }}</a></p>
 {{- end -}}
 {{- end -}}
 
 {{- range (.Data.Pages).GroupByDate "2006" -}}
 {{- if ne .Key "0001" -}}
 <h2 class="head">{{- .Key -}}</h2>
 {{- range .Pages -}}
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="{{ .RelPermalink }}">{{- htmlUnescape .Title -}}</a></h5> <br>
     {{- with .Params.authors -}}by {{ partial "authors.html" (dict "site" $site "authors" .) -}}{{- end -}}
   </div>
   <span class="date">
     {{ .Date.Format "Jan 02" }}
   </span>
 </article>
 {{ end }}
 {{ end }}
 {{ end }}
 {{ end }}
\ No newline at end of file
diff --git a/metadata/topics.toml b/metadata/topics.toml
--- a/metadata/topics.toml
+++ b/metadata/topics.toml
@@ -1,579 +1,579 @@
 ["Computer science"]
 
 ["Computer science".classification]
 ams.id = "68"
 ams.hierarchy = [
   "Computer science",
 ]
 
 ["Computer science"."Artificial intelligence"]
 
 ["Computer science"."Artificial intelligence".classification]
+acm.id = "10010147.10010178"
+acm.desc = "Computing methodologies~Artificial intelligence"
 ams.id = "68T"
 ams.hierarchy = [
   "Computer science",
   "Artificial intelligence",
 ]
-acm.id = "10010147.10010178"
-acm.desc = "Computing methodologies~Artificial intelligence"
 
 ["Computer science"."Automata and formal languages"]
 
 ["Computer science"."Automata and formal languages".classification]
+acm.id = "10003752.10003766"
+acm.desc = "Theory of computation~Formal languages and automata theory"
 ams.id = "68Q45"
 ams.hierarchy = [
   "Computer scienece",
   "Theory of computing",
   "Formal languages and automata",
 ]
-acm.id = "10003752.10003766"
-acm.desc = "Theory of computation~Formal languages and automata theory"
 
 ["Computer science".Algorithms]
 
 ["Computer science".Algorithms.classification]
+acm.id = "10003752.10003809"
+acm.desc = "Theory of computation~Design and analysis of algorithms"
 ams.id = "68W"
 ams.hierarchy = [
   "Computer science",
   "Algorithms in computer science",
 ]
-acm.id = "10003752.10003809"
-acm.desc = "Theory of computation~Design and analysis of algorithms"
 
 ["Computer science".Algorithms.Graph]
 
 ["Computer science".Algorithms.Graph.classification]
+acm.id = "10003752.10003809.10003635"
+acm.desc = "Theory of computation~Graph algorithms analysis"
 ams.id = "05C85"
 ams.hierarchy = [
   "Combinatorics",
   "Graph theory",
   "Graph algorithms",
 ]
-acm.id = "10003752.10003809.10003635"
-acm.desc = "Theory of computation~Graph algorithms analysis"
 
 ["Computer science".Algorithms.Distributed]
 
 ["Computer science".Algorithms.Distributed.classification]
+acm.id = "10003752.10003809.10010172"
+acm.desc = "Theory of computation~Distributed algorithms"
 ams.id = "68W15"
 ams.hierarchy = [
   "Computer science",
   "Algorithms in computer science",
   "Distributed algorithms",
 ]
-acm.id = "10003752.10003809.10010172"
-acm.desc = "Theory of computation~Distributed algorithms"
 
 ["Computer science".Algorithms.Concurrent]
 
 ["Computer science".Algorithms.Concurrent.classification]
+acm.id = "10003752.10003809.10011778"
+acm.desc = "Theory of computation~Concurrent algorithms"
 ams.id = "68W10"
 ams.hierarchy = [
   "Computer science",
   "Algorithms in computer science",
   "Parallel algorithms in computer science",
 ]
-acm.id = "10003752.10003809.10011778"
-acm.desc = "Theory of computation~Concurrent algorithms"
 
 ["Computer science".Algorithms.Online]
 
 ["Computer science".Algorithms.Online.classification]
+acm.id = "10003752.10003809.10010047"
+acm.desc = "Theory of computation~Online algorithms"
 ams.id = "68W27"
 ams.hierarchy = [
   "Computer science",
   "Algorithms in computer science",
   "Online algorithms; streaming algorithms",
 ]
-acm.id = "10003752.10003809.10010047"
-acm.desc = "Theory of computation~Online algorithms"
 
 ["Computer science".Algorithms.Geometry]
 
 ["Computer science".Algorithms.Geometry.classification]
 
 ["Computer science".Algorithms.Approximation]
 
 ["Computer science".Algorithms.Approximation.classification]
+acm.id = "10003752.10003809.10003636"
+acm.desc = "Theory of computation~Approximation algorithms analysis"
 ams.id = "68W25"
 ams.hierarchy = [
   "Computer science",
   "Algorithms in computer science",
   "Approximation algorithms",
 ]
-acm.id = "10003752.10003809.10003636"
-acm.desc = "Theory of computation~Approximation algorithms analysis"
 
 ["Computer science".Algorithms.Mathematical]
 
 ["Computer science".Algorithms.Mathematical.classification]
 
 ["Computer science".Algorithms.Optimization]
 
 ["Computer science".Algorithms.Optimization.classification]
 acm.id = "10003752.10003809.10003716"
 acm.desc = "Theory of computation~Mathematical optimization"
 
 ["Computer science".Algorithms."Quantum computing"]
 
 ["Computer science".Algorithms."Quantum computing".classification]
 ams.id = "68Q12"
 ams.hierarchy = [
   "Computer science",
   "Theory of computing",
   "Quantum algorithms and complexity in the theory of computing",
 ]
 
 ["Computer science".Concurrency]
 
 ["Computer science".Concurrency.classification]
-ams.id = "68Q85"
-ams.hierarchy = [
-  "Computer science",
-  "Theory of computing",
-  "Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)",
-]
 acm.id = "10003752.10003753.10003761"
 acm.desc = "Theory of computation~Concurrency"
-
-["Computer science".Concurrency."Process calculi"]
-
-["Computer science".Concurrency."Process calculi".classification]
 ams.id = "68Q85"
 ams.hierarchy = [
   "Computer science",
   "Theory of computing",
   "Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)",
 ]
+
+["Computer science".Concurrency."Process calculi"]
+
+["Computer science".Concurrency."Process calculi".classification]
 acm.id = "10003752.10003753.10003761.10003764"
 acm.desc = "Theory of computation~Process calculi"
+ams.id = "68Q85"
+ams.hierarchy = [
+  "Computer science",
+  "Theory of computing",
+  "Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)",
+]
 
 ["Computer science"."Data structures"]
 
 ["Computer science"."Data structures".classification]
+acm.id = "10003752.10003809.10010031"
+acm.desc = "Theory of computation~Data structures design and analysis"
 ams.id = "68P05"
 ams.hierarchy = [
   "Computer science",
   "Theory of data",
   "Data structures",
 ]
-acm.id = "10003752.10003809.10010031"
-acm.desc = "Theory of computation~Data structures design and analysis"
 
 ["Computer science"."Functional programming"]
 
 ["Computer science"."Functional programming".classification]
+acm.id = "10011007.10011006.10011008.10011009.10011012"
+acm.desc = "Software and its engineering~Functional languages"
 ams.id = "68N18"
 ams.hierarchy = [
   "Computer science",
   "Theory of software",
   "Functional programming and lambda calculus",
 ]
-acm.id = "10011007.10011006.10011008.10011009.10011012"
-acm.desc = "Software and its engineering~Functional languages"
 
 ["Computer science".Hardware]
 
 ["Computer science".Hardware.classification]
 acm.id = "10010583"
 acm.desc = "Hardware"
 
 ["Computer science"."Machine learning"]
 
 ["Computer science"."Machine learning".classification]
 acm.id = "10010147.10010257"
 acm.desc = "Computing methodologies~Machine learning"
 
 ["Computer science".Networks]
 
 ["Computer science".Networks.classification]
 acm.id = "10003033"
 acm.desc = "Networks"
 
 ["Computer science"."Programming languages"]
 
 ["Computer science"."Programming languages".classification]
+acm.id = "10011007.10011006.10011008"
+acm.desc = "Software and its engineering~General programming languages"
 ams.id = "68N15"
 ams.hierarchy = [
   "Computer science",
   "Theory of software",
   "Theory of programming languages",
 ]
-acm.id = "10011007.10011006.10011008"
-acm.desc = "Software and its engineering~General programming languages"
 
 ["Computer science"."Programming languages"."Language definitions"]
 
 ["Computer science"."Programming languages"."Language definitions".classification]
 acm.id = "10011007.10011006.10011039"
 acm.desc = "Software and its engineering~Formal language definitions"
 
 ["Computer science"."Programming languages"."Lambda calculi"]
 
 ["Computer science"."Programming languages"."Lambda calculi".classification]
+acm.id = "10002950.10003714.10003732.10003733"
+acm.desc = "Mathematics of computing~Lambda calculus"
 ams.id = "68N18"
 ams.hierarchy = [
   "Computer science",
   "Theory of software",
   "Functional programming and lambda calculus",
 ]
-acm.id = "10002950.10003714.10003732.10003733"
-acm.desc = "Mathematics of computing~Lambda calculus"
 
 ["Computer science"."Programming languages"."Type systems"]
 
 ["Computer science"."Programming languages"."Type systems".classification]
 acm.id = "10011007.10011006.10011008.10011024.10011028"
 acm.desc = "Software and its engineering~Data types and structures"
 
 ["Computer science"."Programming languages".Logics]
 
 ["Computer science"."Programming languages".Logics.classification]
 acm.id = "10011007.10011006.10011008.10011009.10011015"
 acm.desc = "Software and its engineering~Constraint and logic languages"
 
 ["Computer science"."Programming languages".Compiling]
 
 ["Computer science"."Programming languages".Compiling.classification]
+acm.id = "10011007.10011006.10011041"
+acm.desc = "Software and its engineering~Compilers"
 ams.id = "68N20"
 ams.hierarchy = [
   "Computer science",
   "Theory of software",
   "Theory of compilers and interpreters",
 ]
-acm.id = "10011007.10011006.10011041"
-acm.desc = "Software and its engineering~Compilers"
 
 ["Computer science"."Programming languages"."Static analysis"]
 
 ["Computer science"."Programming languages"."Static analysis".classification]
 acm.id = "10011007.10010940.10010992.10010998.10011000"
 acm.desc = "Software and its engineering~Automated static analysis"
 
 ["Computer science"."Programming languages".Misc]
 
 ["Computer science"."Programming languages".Misc.classification]
 
 ["Computer science".Security]
 
 ["Computer science".Security.classification]
+acm.id = "10002978"
+acm.desc = "Security and privacy"
 ams.id = "68M25"
 ams.hierarchy = [
   "Computer science",
   "Computer system organization",
   "Computer security",
 ]
-acm.id = "10002978"
-acm.desc = "Security and privacy"
 
 ["Computer science".Security.Cryptography]
 
 ["Computer science".Security.Cryptography.classification]
 acm.id = "10002978.10002979"
 acm.desc = "Security and privacy~Cryptography"
 
 ["Computer science"."Semantics and reasoning"]
 
 ["Computer science"."Semantics and reasoning".classification]
+acm.id = "10003752.10010124"
+acm.desc = "Theory of computation~Semantics and reasoning"
 ams.id = "68Q55"
 ams.hierarchy = [
   "Computer science",
   "Theory of computing",
   "Semantics in the theory of computing",
 ]
-acm.id = "10003752.10010124"
-acm.desc = "Theory of computation~Semantics and reasoning"
 
 ["Computer science"."System description languages"]
 
 ["Computer science"."System description languages".classification]
 acm.id = "10011007.10011006.10011060"
 acm.desc = "Software and its engineering~System description languages"
 
 [Logic]
 
 [Logic.classification]
+acm.id = "10003752.10003790"
+acm.desc = "Theory of computation~Logic"
 ams.id = "03"
 ams.hierarchy = [
   "Mathematical logic and foundations",
 ]
-acm.id = "10003752.10003790"
-acm.desc = "Theory of computation~Logic"
 
 [Logic."Philosophical aspects"]
 
 [Logic."Philosophical aspects".classification]
 ams.id = "03A"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "Philosophical aspects of logic and foundations",
 ]
 
 [Logic."General logic"]
 
 [Logic."General logic".classification]
 ams.id = "03B"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "General logic",
 ]
 
 [Logic."General logic"."Classical propositional logic"]
 
 [Logic."General logic"."Classical propositional logic".classification]
 ams.id = "03B05"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "General logic",
   "Classical propositional logic",
 ]
 
 [Logic."General logic"."Classical first-order logic"]
 
 [Logic."General logic"."Classical first-order logic".classification]
 ams.id = "03B10"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "General logic",
   "Classical first-order logic",
 ]
 
 [Logic."General logic"."Decidability of theories"]
 
 [Logic."General logic"."Decidability of theories".classification]
 ams.id = "03B25"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "General logic",
   "Decidability of theories and sets of sentences",
 ]
 
 [Logic."General logic"."Mechanization of proofs"]
 
 [Logic."General logic"."Mechanization of proofs".classification]
 ams.id = "03B35"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "General logic",
   "Mechanization of proofs and logical operations",
 ]
 
 [Logic."General logic"."Logics of knowledge and belief"]
 
 [Logic."General logic"."Logics of knowledge and belief".classification]
+acm.id = "10010147.10010178.10010187.10010198"
+acm.desc = "Computing methodologies~Reasoning about belief and knowledge"
 ams.id = "03B42"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "General logic",
   "Logics of knowledge and belief (including belief change)",
 ]
-acm.id = "10010147.10010178.10010187.10010198"
-acm.desc = "Computing methodologies~Reasoning about belief and knowledge"
 
 [Logic."General logic"."Temporal logic"]
 
 [Logic."General logic"."Temporal logic".classification]
+acm.id = "10003752.10003790.10003793"
+acm.desc = "Theory of computation~Modal and temporal logics"
 ams.id = "03B44"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "General logic",
   "Temporal logic",
 ]
-acm.id = "10003752.10003790.10003793"
-acm.desc = "Theory of computation~Modal and temporal logics"
 
 [Logic."General logic"."Modal logic"]
 
 [Logic."General logic"."Modal logic".classification]
+acm.id = "10003752.10003790.10003793"
+acm.desc = "Theory of computation~Modal and temporal logics"
 ams.id = "03B45"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "General logic",
   "Modal logic (including the logic of norms)",
 ]
-acm.id = "10003752.10003790.10003793"
-acm.desc = "Theory of computation~Modal and temporal logics"
 
 [Logic."General logic"."Paraconsistent logics"]
 
 [Logic."General logic"."Paraconsistent logics".classification]
 ams.id = "03B53"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "General logic",
   "Paraconsistent logics",
 ]
 
 [Logic.Computability]
 
 [Logic.Computability.classification]
+acm.id = "10003752.10003753.10003754"
+acm.desc = "Theory of computation~Computability"
 ams.id = "03D"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "Computability and recursion theory",
 ]
-acm.id = "10003752.10003753.10003754"
-acm.desc = "Theory of computation~Computability"
 
 [Logic."Set theory"]
 
 [Logic."Set theory".classification]
 ams.id = "03E"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "Set theory",
 ]
 
 [Logic."Proof theory"]
 
 [Logic."Proof theory".classification]
+acm.id = "10003752.10003790.10003792"
+acm.desc = "Theory of computation~Proof theory"
 ams.id = "03F"
 ams.hierarchy = [
   "Mathematical logic and foundations",
   "Proof theory and constructive mathematics",
 ]
-acm.id = "10003752.10003790.10003792"
-acm.desc = "Theory of computation~Proof theory"
 
 [Logic.Rewriting]
 
 [Logic.Rewriting.classification]
 acm.id = "10003752.10003790.10003798"
 acm.desc = "Theory of computation~Equational logic and rewriting"
 
 [Mathematics]
 
 [Mathematics.classification]
 
 [Mathematics.Order]
 
 [Mathematics.Order.classification]
 ams.id = "06"
 ams.hierarchy = [
   "Order, lattices, ordered algebraic structures",
 ]
 
 [Mathematics.Algebra]
 
 [Mathematics.Algebra.classification]
 ams.id = "08"
 ams.hierarchy = [
   "General algebraic systems",
 ]
 
 [Mathematics.Analysis]
 
 [Mathematics.Analysis.classification]
 acm.id = "10002950.10003714"
 acm.desc = "Mathematics of computing~Mathematical analysis"
 
 [Mathematics."Measure and integration"]
 
 [Mathematics."Measure and integration".classification]
 ams.id = "28"
 ams.hierarchy = [
   "Measure and integration",
 ]
 
 [Mathematics."Probability theory"]
 
 [Mathematics."Probability theory".classification]
+acm.id = "10002950.10003648"
+acm.desc = "Mathematics of computing~Probability and statistics"
 ams.id = "60"
 ams.hierarchy = [
   "Probability theory and stochastic processes",
 ]
-acm.id = "10002950.10003648"
-acm.desc = "Mathematics of computing~Probability and statistics"
 
 [Mathematics."Number theory"]
 
 [Mathematics."Number theory".classification]
 ams.id = "11"
 ams.hierarchy = [
   "Number theory",
 ]
 
 [Mathematics."Games and economics"]
 
 [Mathematics."Games and economics".classification]
 ams.id = "91"
 ams.hierarchy = [
   "Game theory, economics, finance, and other social and behavioral sciences",
 ]
 
 [Mathematics.Geometry]
 
 [Mathematics.Geometry.classification]
 ams.id = "51"
 ams.hierarchy = [
   "Geometry",
 ]
 
 [Mathematics.Topology]
 
 [Mathematics.Topology.classification]
+acm.id = "10002950.10003741.10003742"
+acm.desc = "Mathematics of computing~Topology"
 ams.id = "54"
 ams.hierarchy = [
   "General topology",
 ]
-acm.id = "10002950.10003741.10003742"
-acm.desc = "Mathematics of computing~Topology"
 
 [Mathematics."Graph theory"]
 
 [Mathematics."Graph theory".classification]
+acm.id = "10002950.10003624.10003633"
+acm.desc = "Mathematics of computing~Graph theory"
 ams.id = "05C"
 ams.hierarchy = [
   "Combinatorics",
   "Graph theory",
 ]
-acm.id = "10002950.10003624.10003633"
-acm.desc = "Mathematics of computing~Graph theory"
 
 [Mathematics.Combinatorics]
 
 [Mathematics.Combinatorics.classification]
+acm.id = "10002950.10003624.10003625"
+acm.desc = "Mathematics of computing~Combinatorics"
 ams.id = "05"
 ams.hierarchy = [
   "Combinatorics",
 ]
-acm.id = "10002950.10003624.10003625"
-acm.desc = "Mathematics of computing~Combinatorics"
 
 [Mathematics."Category theory"]
 
 [Mathematics."Category theory".classification]
 ams.id = "18"
 ams.hierarchy = [
   "Category theory; homological algebra",
 ]
 
 [Mathematics.Physics]
 
 [Mathematics.Physics.classification]
 ams.id = "00A79"
 ams.hierarchy = [
   "General and overarching topics; collections",
   "General applied mathematics",
   "Physics",
 ]
 
 [Mathematics.Physics."Quantum information"]
 
 [Mathematics.Physics."Quantum information".classification]
+acm.id = "10003752.10003753.10003758.10010626"
+acm.desc = "Theory of computation~Quantum information theory"
 ams.id = "81P45"
 ams.hierarchy = [
   "Quantum theory",
   "Foundations, quantum information and its processing, quantum axioms, and philosophy",
   "Quantum information, communication, networks (quantum-theoretic aspects)",
 ]
-acm.id = "10003752.10003753.10003758.10010626"
-acm.desc = "Theory of computation~Quantum information theory"
 
 [Mathematics.Misc]
 
 [Mathematics.Misc.classification]
 
 [Tools]
 
 [Tools.classification]