diff --git a/thys/Transition_Systems_and_Automata/ROOT b/thys/Transition_Systems_and_Automata/ROOT
--- a/thys/Transition_Systems_and_Automata/ROOT
+++ b/thys/Transition_Systems_and_Automata/ROOT
@@ -1,38 +1,42 @@
 chapter AFP
 
 session Transition_Systems_and_Automata (AFP) = "Collections" +
   options [timeout = 2400]
   sessions
     "DFS_Framework"
     "Gabow_SCC"
   directories
     "Basic"
     "Transition_Systems"
     "Automata"
+    "Automata/DFA"
+    "Automata/NFA"
     "Automata/DBA"
+    "Automata/DBTA"
     "Automata/DCA"
-    "Automata/DFA"
     "Automata/DRA"
     "Automata/NBA"
-    "Automata/NFA"
+    "Automata/NBTA"
   theories
     "Basic/Basic"
     "Basic/Sequence"
     "Basic/Sequence_Zip"
     "Basic/Sequence_LTL"
     "Basic/Maps"
     "Basic/Acceptance"
     "Transition_Systems/Transition_System"
     "Transition_Systems/Transition_System_Extra"
     "Transition_Systems/Transition_System_Construction"
     "Automata/DFA/DFA"
     "Automata/NFA/NFA"
+    "Automata/DBA/DBA_Combine"
+    "Automata/DBTA/DBTA_Combine"
+    "Automata/DCA/DCA_Combine"
+    "Automata/DRA/DRA_Combine"
+    "Automata/DRA/DRA_Translate"
     "Automata/NBA/NBA_Combine"
     "Automata/NBA/NBA_Translate"
     "Automata/NBA/NGBA_Algorithms"
-    "Automata/DBA/DBA_Combine"
-    "Automata/DCA/DCA_Combine"
-    "Automata/DRA/DRA_Combine"
-    "Automata/DRA/DRA_Translate"
+    "Automata/NBTA/NBTA_Combine"
   document_files
     "root.tex"