diff --git a/thys/Van_Emde_Boas_Trees/ROOT b/thys/Van_Emde_Boas_Trees/ROOT
--- a/thys/Van_Emde_Boas_Trees/ROOT
+++ b/thys/Van_Emde_Boas_Trees/ROOT
@@ -1,42 +1,37 @@
 chapter AFP
 
 session Van_Emde_Boas_Trees (AFP) = HOL +
   (*descpription "Functional and imperative van Emde Boas Trees"*)
   options [timeout = 900]
   sessions
     "HOL-Imperative_HOL"
     "Automatic_Refinement"
      Deriving
-directories
+  directories
     Imperative_HOL_Time
     Separation_Logic_Imperative_HOL
     "Separation_Logic_Imperative_HOL/Tools"
     Time_Reasoning
   (*suppression of some theories*)
-
   theories [document = false]
     "Imperative_HOL_Time/Array_Time"
     "Imperative_HOL_Time/Heap"
     "Imperative_HOL_Time/Heap_Time_Monad"
     "Imperative_HOL_Time/Imperative_HOL_Time"
     "Imperative_HOL_Time/Ref_Time"
     "Separation_Logic_Imperative_HOL/Assertions"
     "Separation_Logic_Imperative_HOL/Automation"
     "Separation_Logic_Imperative_HOL/Hoare_Triple"
     "Separation_Logic_Imperative_HOL/Refine_Imp_Hol"
     "Separation_Logic_Imperative_HOL/Sep_Main"
     "Separation_Logic_Imperative_HOL/Tools/Imperative_HOL_Add"
     "Separation_Logic_Imperative_HOL/Tools/Syntax_Match"
-
   theories [document = false]
-    VEBT_Example_Setup  
+    VEBT_Example_Setup
     "Time_Reasoning/Simple_TBOUND_Cond"
-  
   theories
     VEBT_Intf_Imperative
     VEBT_Example
-
   document_files
     "root.bib"
     "root.tex"
-