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,50 +1,51 @@
 {{- 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="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="https://www.isa-afp.org/">front page</a>.
 </strong>
 </p>
+{{- else -}}
+<p>
+  A <a href="https://devel.isa-afp.org/">development version</a> of the archive is available as well.
+</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/partials/theory-navigation.html b/admin/site/themes/afp/layouts/partials/theory-navigation.html
--- a/admin/site/themes/afp/layouts/partials/theory-navigation.html
+++ b/admin/site/themes/afp/layouts/partials/theory-navigation.html
@@ -1,39 +1,32 @@
 {{- $entry_name := .Params.entry -}}
 {{- $site := . -}}
 {{- $path := .Site.Params.afpUrls.html -}}
 {{- if isset .Site.Data "status" -}}
   {{- $path = .Site.Params.afpUrls.htmlDevel -}}
 {{- end -}}
 <div id="menu-toggle">
   <input id="toggle" type="checkbox" />
   <label for="toggle">
     <span>menu</span>
     <img src="{{- .Site.BaseURL -}}images/menu.svg" alt="Menu" />
   </label>
 
   <a href="{{- .Site.BaseURL -}}" class='logo-link'>
     <img src="{{- .Site.BaseURL -}}images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
   </a>
 
   <nav id="menu">
   <div>
     <a href="{{- .Site.BaseURL -}}" class='logo-link'>
       <img src="{{- .Site.BaseURL -}}images/afp.png" alt='Logo of the Archive of Formal Proofs'
         class="logo">
     </a>
     {{ $currentPage := . -}}
     <ul id="return">
       <li><a href="{{- .Site.BaseURL -}}entries/{{- $entry_name -}}.html">Return to entry</a></li>
     </ul>
     <hr>
     <ul id="theory-navbar" class="list-group"></ul>
   </div>
-  <ul>
-    <li><a href="{{- $path -}}/{{- $entry_name -}}/outline.pdf">Proof
-      outline</a></li>
-    <li><a href="{{- $path -}}/{{- $entry_name -}}/document.pdf">Proof
-      document</a></li>
-    <li><a href="{{- $path -}}/{{- $entry_name -}}/session_graph.pdf">Session dependencies</a></li>
-  </ul>
   </nav>
 </div>