--- a
+++ b/thys/TLA/ROOT.ML
@@ -0,0 +1,20 @@
+(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
+    Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
+                 Stephan Merz <Stephan.Merz at loria.fr>
+    Year:        2011
+    Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
+*)
+
+use_thys [
+  "Sequence",
+  "Intensional",
+  "Semantics",
+  "PreFormulas",
+  "Rules",
+  "Liveness",
+  "State",
+  "Even",
+  "Inc",
+  "Buffer"
+];
+