diff --git a/thys/Clean/ROOT b/thys/Clean/ROOT
--- a/thys/Clean/ROOT
+++ b/thys/Clean/ROOT
@@ -1,63 +1,63 @@
 (******************************************************************************
  * Clean
  *
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are
  * met:
  *
  *     * Redistributions of source code must retain the above copyright
  *       notice, this list of conditions and the following disclaimer.
  *
  *     * Redistributions in binary form must reproduce the above
  *       copyright notice, this list of conditions and the following
  *       disclaimer in the documentation and/or other materials provided
  *       with the distribution.
  *
  *     * Neither the name of the copyright holders nor the names of its
  *       contributors may be used to endorse or promote products derived
  *       from this software without specific prior written permission.
  *
  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
  * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
  * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
  * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
  * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
  * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
  * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
  * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  ******************************************************************************)
 
 (*
  * Clean --- a basic abstract ("shallow") programming language for test and proof.
  * Authors : Burkhart Wolff, Frédéric Tuong
  *)
 
-
+chapter AFP
 
 session Clean (AFP) = HOL +
   options [timeout=300, document = pdf, document_output = "output"]
   sessions
-    "HOL-Eisbach" 
+    "HOL-Eisbach"
     "HOL-Computational_Algebra"
   directories
     "src"
-    "examples" 
+    "examples"
   theories
     "src/Clean_Main"
     "examples/IsPrime"
-    "examples/LinearSearch" 
+    "examples/LinearSearch"
     "examples/Quicksort"
     "examples/Quicksort_concept"
     "examples/SquareRoot_concept"
   document_files
     "root.tex"
     "root.bib"
     "lstisadof.sty"